| changeset 36176 | 3fe7e97ccca8 |
| parent 27318 | 5cd16e4df9c2 |
| child 39795 | 9e59b4c11039 |
--- a/doc-src/TutorialI/Datatype/Nested.thy Fri Apr 16 20:56:40 2010 +0200 +++ b/doc-src/TutorialI/Datatype/Nested.thy Fri Apr 16 21:28:09 2010 +0200 @@ -11,7 +11,7 @@ Consider the following model of terms where function symbols can be applied to a list of arguments: *} -(*<*)hide const Var(*>*) +(*<*)hide_const Var(*>*) datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term list"; text{*\noindent