doc-src/TutorialI/Documents/Documents.thy

   imports Main
   begin
 
   subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
 
-  consts
-    foo :: \dots
-    bar :: \dots
-
-  defs \dots
+  definition foo :: \dots
+
+  definition bar :: \dots
 
   subsection {\ttlbrace}* Derived rules *{\ttrbrace}
 
   lemma fooI: \dots
   lemma fooE: \dots