diff -r afc1dfc5a92d -r cd89ce2795ab src/HOL/NumberTheory/Fib.ML --- a/src/HOL/NumberTheory/Fib.ML Tue Jan 23 15:47:36 2001 +0100 +++ b/src/HOL/NumberTheory/Fib.ML Tue Jan 23 15:48:35 2001 +0100 @@ -50,8 +50,8 @@ (*Concrete Mathematics, page 278: Cassini's identity. It is much easier to prove using integers!*) Goal "int (fib (Suc (Suc n)) * fib n) = \ -\ (if n mod 2 = 0 then int (fib(Suc n) * fib(Suc n)) - #1 \ -\ else int (fib(Suc n) * fib(Suc n)) + #1)"; +\ (if n mod #2 = 0 then int (fib(Suc n) * fib(Suc n)) - #1 \ +\ else int (fib(Suc n) * fib(Suc n)) + #1)"; by (induct_thm_tac fib.induct "n" 1); by (simp_tac (simpset() addsimps [fib_Suc_Suc, mod_Suc]) 2); by (simp_tac (simpset() addsimps [fib_Suc_Suc]) 1);