# HG changeset patch
# User nipkow
# Date 1223983447 -7200
# Node ID 58ac551ce1ce1323f195fe40f8443f50a26eea0f
# Parent  9bb9791bdc18b62fb6fbab1f81c47b876fe9ca92
added lemma

diff -r 9bb9791bdc18 -r 58ac551ce1ce 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 *}