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}