--- a/doc-src/TutorialI/Recdef/Nested1.thy Fri Sep 28 18:55:37 2001 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy Fri Sep 28 19:17:01 2001 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory Nested1 = Nested0:;
+theory Nested1 = Nested0:
(*>*)
text{*\noindent
@@ -11,11 +11,11 @@
Defining @{term trev} by \isacommand{recdef} rather than \isacommand{primrec}
simplifies matters because we are now free to use the recursion equation
suggested at the end of \S\ref{sec:nested-datatype}:
-*};
+*}
-recdef trev "measure size"
+recdef (*<*)(permissive)(*<*)trev "measure size"
"trev (Var x) = Var x"
- "trev (App f ts) = App f (rev(map trev ts))";
+ "trev (App f ts) = App f (rev(map trev ts))"
text{*\noindent
Remember that function @{term size} is defined for each \isacommand{datatype}.
@@ -34,8 +34,8 @@
which equals @{term"Suc(term_list_size ts)"}. We will now prove the termination condition and
continue with our definition. Below we return to the question of how
\isacommand{recdef} knows about @{term map}.
-*};
+*}
(*<*)
-end;
+end
(*>*)