# HG changeset patch
# User paulson
# Date 1079689460 -3600
# Node ID 846c237bd9b3d33f21baf907e1a23e92f7a99499
# Parent  cba7c0a3ffb3bf34c9ecb32c1896ae52ff1efe78
stylistic tweaks

diff -r cba7c0a3ffb3 -r 846c237bd9b3 src/HOL/Integ/Bin.thy
--- 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)
diff -r cba7c0a3ffb3 -r 846c237bd9b3 src/HOL/Integ/IntArith.thy
--- 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]:
diff -r cba7c0a3ffb3 -r 846c237bd9b3 src/HOL/Integ/IntDiv.thy
--- 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
diff -r cba7c0a3ffb3 -r 846c237bd9b3 src/HOL/Integ/Parity.thy
--- 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