changeset 9992 | 4281ccea43f0 |
parent 9933 | 9feb1e0c4cb3 |
child 10171 | 59d6633835fa |
--- a/doc-src/TutorialI/Recdef/termination.thy Fri Sep 15 19:34:28 2000 +0200 +++ b/doc-src/TutorialI/Recdef/termination.thy Fri Sep 15 19:59:05 2000 +0200 @@ -47,7 +47,7 @@ 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 simp: termi_lem) +(hints recdef_simp: termi_lem) text{*\noindent This time everything works fine. Now @{thm[source]g.simps} contains precisely