--- a/src/HOL/Integ/Parity.thy Fri Mar 19 10:42:38 2004 +0100
+++ b/src/HOL/Integ/Parity.thy Fri Mar 19 10:44:20 2004 +0100
@@ -267,12 +267,12 @@
(is "?P n")
proof cases
assume even: "even n"
- from this obtain k where "n = 2*k"
+ then obtain k where "n = 2*k"
by (auto simp add: even_nat_equiv_def2 numeral_2_eq_2)
thus ?thesis by (simp add: zero_le_even_power even)
next
assume odd: "odd n"
- from this obtain k where "n = Suc(2*k)"
+ then obtain k where "n = Suc(2*k)"
by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2)
thus ?thesis
by (auto simp add: power_Suc zero_le_mult_iff zero_le_even_power