src/HOL/NumberTheory/Fib.thy

--- 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