src/HOL/NumberTheory/Fib.thy
changeset 11704 3c50a2cd6f00
parent 11701 3d51fbf81c17
child 11786 51ce34ef5113
     1.1 --- a/src/HOL/NumberTheory/Fib.thy	Fri Oct 05 23:58:52 2001 +0200
     1.2 +++ b/src/HOL/NumberTheory/Fib.thy	Sat Oct 06 00:02:46 2001 +0200
     1.3 @@ -67,14 +67,14 @@
     1.4  *}
     1.5  
     1.6  lemma fib_Cassini: "int (fib (Suc (Suc n)) * fib n) =
     1.7 -  (if n mod # 2 = 0 then int (fib (Suc n) * fib (Suc n)) - Numeral1
     1.8 +  (if n mod 2 = 0 then int (fib (Suc n) * fib (Suc n)) - Numeral1
     1.9     else int (fib (Suc n) * fib (Suc n)) + Numeral1)"
    1.10    apply (induct n rule: fib.induct)
    1.11      apply (simp add: fib.Suc_Suc)
    1.12     apply (simp add: fib.Suc_Suc mod_Suc)
    1.13    apply (simp add: fib.Suc_Suc
    1.14      add_mult_distrib add_mult_distrib2 mod_Suc zmult_int [symmetric] zmult_ac)
    1.15 -  apply (subgoal_tac "x mod # 2 < # 2", arith)
    1.16 +  apply (subgoal_tac "x mod 2 < 2", arith)
    1.17    apply simp
    1.18    done
    1.19