--- a/src/HOL/NumberTheory/Fib.thy Fri Nov 09 13:41:27 2007 +0100
+++ b/src/HOL/NumberTheory/Fib.thy Fri Nov 09 18:59:56 2007 +0100
@@ -43,7 +43,7 @@
next
case 2 show ?case by (simp add: fib_2)
next
- case fib_2 thus ?case by (simp add: fib.simps add_mult_distrib2)
+ case 3 thus ?case by (simp add: fib_2 add_mult_distrib2)
qed
lemma fib_Suc_neq_0: "fib (Suc n) \<noteq> 0"
@@ -72,9 +72,9 @@
next
case 2 thus ?case by (simp add: fib_2 mod_Suc)
next
- case (fib_2 x)
+ case (3 x)
have "Suc 0 \<noteq> x mod 2 \<longrightarrow> x mod 2 = 0" by presburger
- with "fib_2.hyps" show ?case by (simp add: fib.simps add_mult_distrib add_mult_distrib2)
+ with "3.hyps" show ?case by (simp add: fib.simps add_mult_distrib add_mult_distrib2)
qed
text{*We now obtain a version for the natural numbers via the coercion