2 to #2
authorpaulson
Tue, 23 Jan 2001 15:48:35 +0100
changeset 10965 cd89ce2795ab
parent 10964 afc1dfc5a92d
child 10966 8f2c27041a8e
2 to #2
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);