From b707eff08d8c9b610bfe5f57626c69ae2fca8a1b Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Sat, 17 Aug 2019 10:48:15 +0200
Subject: [PATCH] bug in article class.

---
 .../technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy   | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy
index 70faafab..afad80ca 100644
--- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy
+++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy
@@ -392,9 +392,8 @@ text\<open>
 
 \begin{isar}
 doc_class article = 
-   trace :: "(title + subtitle + author+ abstract +
-              introduction + technical + example +
-              conclusion + bibliography) list"
+   style_id :: string                <= "''LNCS''"
+   version  :: "(int \<times> int \<times> int)"  <= "(0,0,0)"
    where "(title       ~~ \<lbrakk>subtitle\<rbrakk>   ~~ \<lbrace>author\<rbrace>$^+$+  ~~  abstract    ~~
              introduction ~~  \<lbrace>technical || example\<rbrace>$^+$  ~~  conclusion ~~  
              bibliography)"