| changeset 11636 | 0bec857c9871 |
| parent 11626 | 0dbfb578bf75 |
| child 12491 | e28870d8b223 |
--- a/doc-src/TutorialI/Recdef/Nested1.thy Fri Sep 28 20:08:05 2001 +0200 +++ b/doc-src/TutorialI/Recdef/Nested1.thy Fri Sep 28 20:08:28 2001 +0200 @@ -13,7 +13,7 @@ suggested at the end of \S\ref{sec:nested-datatype}: *} -recdef (*<*)(permissive)(*<*)trev "measure size" +recdef (*<*)(permissive)(*>*)trev "measure size" "trev (Var x) = Var x" "trev (App f ts) = App f (rev(map trev ts))"