diff -r 3602b81665b5 -r 63f0b638355c doc-src/TutorialI/Documents/Documents.thy
--- 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}