--- a/src/HOL/Integ/Bin.thy Fri Mar 19 10:42:38 2004 +0100
+++ b/src/HOL/Integ/Bin.thy Fri Mar 19 10:44:20 2004 +0100
@@ -159,7 +159,7 @@
lemma Ints_odd_nonzero: "a \<in> Ints ==> 1 + a + a \<noteq> (0::'a::ordered_ring)"
proof (unfold Ints_def)
assume "a \<in> range of_int"
- from this obtain z where a: "a = of_int z" ..
+ then obtain z where a: "a = of_int z" ..
show ?thesis
proof
assume eq: "1 + a + a = 0"
@@ -233,7 +233,7 @@
"a \<in> Ints ==> (1 + a + a < 0) = (a < (0::'a::ordered_ring))";
proof (unfold Ints_def)
assume "a \<in> range of_int"
- from this obtain z where a: "a = of_int z" ..
+ then obtain z where a: "a = of_int z" ..
hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
by (simp add: prems)
also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
--- a/src/HOL/Integ/IntArith.thy Fri Mar 19 10:42:38 2004 +0100
+++ b/src/HOL/Integ/IntArith.thy Fri Mar 19 10:44:20 2004 +0100
@@ -275,7 +275,7 @@
from step[OF ki1 this] show ?case by simp
qed
}
- from this ge show ?thesis by fast
+ with ge show ?thesis by fast
qed
(* `set:int': dummy construction *)
@@ -311,7 +311,7 @@
from step[OF ki1 this] show ?case by simp
qed
}
- from this le show ?thesis by fast
+ with le show ?thesis by fast
qed
theorem int_less_induct [consumes 1,case_names base step]:
--- a/src/HOL/Integ/IntDiv.thy Fri Mar 19 10:42:38 2004 +0100
+++ b/src/HOL/Integ/IntDiv.thy Fri Mar 19 10:44:20 2004 +0100
@@ -624,7 +624,7 @@
lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
proof
assume "m mod d = 0"
- from this zmod_zdiv_equality[of m d] show "EX q::int. m = d*q" by auto
+ with zmod_zdiv_equality[of m d] show "EX q::int. m = d*q" by auto
next
assume "EX q::int. m = d*q"
thus "m mod d = 0" by auto
--- 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