src/HOL/ex/Fundefs.thy

--- a/src/HOL/ex/Fundefs.thy	Tue Oct 14 13:23:31 2008 +0200
+++ b/src/HOL/ex/Fundefs.thy	Tue Oct 14 13:24:07 2008 +0200
@@ -87,7 +87,9 @@
   with `~ 100 < n` show "(f91 (n + 11), n) : ?R" by simp 
 qed
 
-
+text{* Now trivial (even though it does not belong here): *}
+lemma "f91 n = (if 100 < n then n - 10 else 91)"
+by (induct n rule:f91.induct) auto
 
 
 subsection {* More general patterns *}