diff -r 74cdf24724ea -r 0dbfb578bf75 doc-src/TutorialI/Recdef/termination.thy
--- a/doc-src/TutorialI/Recdef/termination.thy	Fri Sep 28 18:55:37 2001 +0200
+++ b/doc-src/TutorialI/Recdef/termination.thy	Fri Sep 28 19:17:01 2001 +0200
@@ -16,9 +16,9 @@
 Isabelle may fail to prove the termination condition for some
 recursive call.  Let us try the following artificial function:*}
 
-consts f :: "nat\<times>nat \<Rightarrow> nat";
-recdef f "measure(\<lambda>(x,y). x-y)"
-  "f(x,y) = (if x \<le> y then x else f(x,y+1))";
+consts f :: "nat\<times>nat \<Rightarrow> nat"
+recdef (*<*)(permissive)(*<*)f "measure(\<lambda>(x,y). x-y)"
+  "f(x,y) = (if x \<le> y then x else f(x,y+1))"
 
 text{*\noindent
 Isabelle prints a
@@ -28,14 +28,14 @@
 of your function once more. In our case the required lemma is the obvious one:
 *}
 
-lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y";
+lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y"
 
 txt{*\noindent
 It was not proved automatically because of the awkward behaviour of subtraction
 on type @{typ"nat"}. This requires more arithmetic than is tried by default:
 *}
 
-apply(arith);
+apply(arith)
 done
 
 text{*\noindent
@@ -45,7 +45,7 @@
 a simplification rule.  
 *}
 
-consts g :: "nat\<times>nat \<Rightarrow> nat";
+consts g :: "nat\<times>nat \<Rightarrow> nat"
 recdef g "measure(\<lambda>(x,y). x-y)"
   "g(x,y) = (if x \<le> y then x else g(x,y+1))"
 (hints recdef_simp: termi_lem)
@@ -56,8 +56,8 @@
 simplification rule.  Thus we can automatically prove results such as this one:
 *}
 
-theorem "g(1,0) = g(1,1)";
-apply(simp);
+theorem "g(1,0) = g(1,1)"
+apply(simp)
 done
 
 text{*\noindent