doc-src/TutorialI/Documents/Documents.thy
changeset 27027 63f0b638355c
parent 27015 f8537d69f514
child 28504 7ad7d7d6df47
--- a/doc-src/TutorialI/Documents/Documents.thy	Fri May 30 17:03:37 2008 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy	Fri May 30 17:52:10 2008 +0200
@@ -474,11 +474,9 @@
 
   subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
 
-  consts
-    foo :: \dots
-    bar :: \dots
+  definition foo :: \dots
 
-  defs \dots
+  definition bar :: \dots
 
   subsection {\ttlbrace}* Derived rules *{\ttrbrace}