1.1 --- a/doc-src/TutorialI/Recdef/termination.thy	Fri Sep 15 19:34:28 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/termination.thy	Fri Sep 15 19:59:05 2000 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4  consts g :: "nat\<times>nat \<Rightarrow> nat";
     1.5  recdef g "measure(\<lambda>(x,y). x-y)"
     1.6    "g(x,y) = (if x \<le> y then x else g(x,y+1))"
     1.7 -(hints simp: termi_lem)
     1.8 +(hints recdef_simp: termi_lem)
     1.9  
    1.10  text{*\noindent
    1.11  This time everything works fine. Now @{thm[source]g.simps} contains precisely