# HG changeset patch
# User nipkow
# Date 881424381 -3600
# Node ID 7049ca8f912e1e885b5f2429335064845cf2fc60
# Parent  e52f864c5b884ff465244d2d472a0a981342e6f2
Replaced Fib(Suc n)~=0 by 0<Fib(Suc(n)).

diff -r e52f864c5b88 -r 7049ca8f912e src/HOL/ex/Fib.ML
--- a/src/HOL/ex/Fib.ML	Sat Dec 06 17:05:41 1997 +0100
+++ b/src/HOL/ex/Fib.ML	Sat Dec 06 17:06:21 1997 +0100
@@ -39,6 +39,12 @@
 qed "fib_Suc_neq_0";
 Addsimps [fib_Suc_neq_0];
 
+goal thy "0 < fib (Suc n)";
+by (res_inst_tac [("u","n")] fib.induct 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps fib.rules)));
+qed "fib_Suc_gr_0";
+Addsimps [fib_Suc_gr_0];
+
 
 
 (*Concrete Mathematics, page 278: Cassini's identity*)