changeset 23365 | f31794033ae1 |
parent 23315 | df3a7e9ebadb |
child 23431 | 25ca91279a9b |
--- a/src/HOL/NumberTheory/Fib.thy Wed Jun 13 03:28:21 2007 +0200 +++ b/src/HOL/NumberTheory/Fib.thy Wed Jun 13 03:31:11 2007 +0200 @@ -85,7 +85,7 @@ (if n mod 2 = 0 then fib (Suc n) * fib (Suc n) - 1 else fib (Suc n) * fib (Suc n) + 1)" apply (rule int_int_eq [THEN iffD1]) - apply (simp add: fib_Cassini_int) + apply (simp add: fib_Cassini_int del: of_nat_mult) apply (subst zdiff_int [symmetric]) apply (insert fib_Suc_gr_0 [of n], simp_all) done