--- a/src/HOL/ex/Fundefs.thy Sat Sep 15 19:27:35 2007 +0200
+++ b/src/HOL/ex/Fundefs.thy Sat Sep 15 19:27:40 2007 +0200
@@ -70,7 +70,7 @@
(* Prove a lemma before attempting a termination proof *)
lemma f91_estimate:
- assumes trm: "f91_dom n"
+ assumes trm: "f91_dom n"
shows "n < f91 n + 11"
using trm by induct auto
@@ -80,7 +80,7 @@
show "wf ?R" ..
fix n::nat assume "~ 100 < n" (* Inner call *)
- thus "(n + 11, n) : ?R" by simp
+ thus "(n + 11, n) : ?R" by simp
assume inner_trm: "f91_dom (n + 11)" (* Outer call *)
with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
@@ -89,6 +89,7 @@
+
subsection {* More general patterns *}
subsubsection {* Overlapping patterns *}