diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Library/Rational_Numbers.thy
--- a/src/HOL/Library/Rational_Numbers.thy	Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Library/Rational_Numbers.thy	Mon Jan 12 16:51:45 2004 +0100
@@ -1,7 +1,7 @@
-(*  Title:      HOL/Library/Rational_Numbers.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+(*  Title: HOL/Library/Rational_Numbers.thy
+    ID:    $Id$
+    Author: Markus Wenzel, TU Muenchen
+    License: GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 header {*
@@ -85,7 +85,7 @@
       next
         assume a': "a' \<noteq> 0"
         from eq1 eq2 have "(a * b') * (a' * b'') = (a' * b) * (a'' * b')" by simp
-        hence "(a * b'') * (a' * b') = (a'' * b) * (a' * b')" by (simp only: zmult_ac)
+        hence "(a * b'') * (a' * b') = (a'' * b) * (a' * b')" by (simp only: mult_ac)
         with a' b' show ?thesis by simp
       qed
       thus "fract a b \<sim> fract a'' b''" ..
@@ -152,11 +152,11 @@
       (is "?lhs = ?rhs")
     proof -
       have "?lhs = (a * b') * (d * d') + (c * d') * (b * b')"
-        by (simp add: int_distrib zmult_ac)
+        by (simp add: int_distrib mult_ac)
       also have "... = (a' * b) * (d * d') + (c' * d) * (b * b')"
         by (simp only: eq1 eq2)
       also have "... = ?rhs"
-        by (simp add: int_distrib zmult_ac)
+        by (simp add: int_distrib mult_ac)
       finally show "?lhs = ?rhs" .
     qed
     from neq show "b * d \<noteq> 0" by simp
@@ -188,7 +188,7 @@
   have "\<lfloor>fract (a * c) (b * d)\<rfloor> = \<lfloor>fract (a' * c') (b' * d')\<rfloor>"
   proof
     from eq1 eq2 have "(a * b') * (c * d') = (a' * b) * (c' * d)" by simp
-    thus "(a * c) * (b' * d') = (a' * c') * (b * d)" by (simp add: zmult_ac)
+    thus "(a * c) * (b' * d') = (a' * c') * (b * d)" by (simp add: mult_ac)
     from neq show "b * d \<noteq> 0" by simp
     from neq show "b' * d' \<noteq> 0" by simp
   qed
@@ -206,7 +206,7 @@
   with neq obtain "a \<noteq> 0" and "a' \<noteq> 0" by (simp add: is_zero_fraction_iff)
   assume "\<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor>"
   hence "a * b' = a' * b" ..
-  hence "b * a' = b' * a" by (simp only: zmult_ac)
+  hence "b * a' = b' * a" by (simp only: mult_ac)
   hence "\<lfloor>fract b a\<rfloor> = \<lfloor>fract b' a'\<rfloor>" ..
   with neq show ?thesis by (simp add: inverse_fraction_def)
 qed
@@ -225,12 +225,12 @@
     fix a b c d x :: int assume x: "x \<noteq> 0"
     have "?le a b c d = ?le (a * x) (b * x) c d"
     proof -
-      from x have "0 < x * x" by (auto simp add: int_less_le)
+      from x have "0 < x * x" by (auto simp add: zero_less_mult_iff)
       hence "?le a b c d =
           ((a * d) * (b * d) * (x * x) \<le> (c * b) * (b * d) * (x * x))"
-        by (simp add: zmult_zle_cancel2)
+        by (simp add: mult_le_cancel_right)
       also have "... = ?le (a * x) (b * x) c d"
-        by (simp add: zmult_ac)
+        by (simp add: mult_ac)
       finally show ?thesis .
     qed
   } note le_factor = this
@@ -241,11 +241,11 @@
   hence "?le a b c d = ?le (a * ?D') (b * ?D') c d"
     by (rule le_factor)
   also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')"
-    by (simp add: zmult_ac)
+    by (simp add: mult_ac)
   also have "... = ((a' * b) * ?D * ?D' * d * d' \<le> (c' * d) * ?D * ?D' * b * b')"
     by (simp only: eq1 eq2)
   also have "... = ?le (a' * ?D) (b' * ?D) c' d'"
-    by (simp add: zmult_ac)
+    by (simp add: mult_ac)
   also from D have "... = ?le a' b' c' d'"
     by (rule le_factor [symmetric])
   finally have "?le a b c d = ?le a' b' c' d'" .
@@ -470,14 +470,15 @@
 
 theorem abs_rat: "b \<noteq> 0 ==> \<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
   by (simp add: abs_rat_def minus_rat zero_rat less_rat eq_rat)
-    (auto simp add: zmult_less_0_iff int_0_less_mult_iff int_le_less split: zabs_split)
+     (auto simp add: mult_less_0_iff zero_less_mult_iff int_le_less 
+                split: abs_split)
 
 
 subsubsection {* The ordered field of rational numbers *}
 
 lemma rat_add_assoc: "(q + r) + s = q + (r + (s::rat))"
   by (induct q, induct r, induct s) 
-     (simp add: add_rat zadd_ac zmult_ac int_distrib)
+     (simp add: add_rat add_ac mult_ac int_distrib)
 
 lemma rat_add_0: "0 + q = (q::rat)"
   by (induct q) (simp add: zero_rat add_rat)
@@ -492,7 +493,7 @@
   show "(q + r) + s = q + (r + s)"
     by (rule rat_add_assoc)
   show "q + r = r + q"
-    by (induct q, induct r) (simp add: add_rat zadd_ac zmult_ac)
+    by (induct q, induct r) (simp add: add_rat add_ac mult_ac)
   show "0 + q = q"
     by (induct q) (simp add: zero_rat add_rat)
   show "(-q) + q = 0"
@@ -500,9 +501,9 @@
   show "q - r = q + (-r)"
     by (induct q, induct r) (simp add: add_rat minus_rat diff_rat)
   show "(q * r) * s = q * (r * s)"
-    by (induct q, induct r, induct s) (simp add: mult_rat zmult_ac)
+    by (induct q, induct r, induct s) (simp add: mult_rat mult_ac)
   show "q * r = r * q"
-    by (induct q, induct r) (simp add: mult_rat zmult_ac)
+    by (induct q, induct r) (simp add: mult_rat mult_ac)
   show "1 * q = q"
     by (induct q) (simp add: one_rat mult_rat)
   show "(q + r) * s = q * s + r * s"
@@ -533,25 +534,25 @@
       show "Fract a b \<le> Fract e f"
       proof -
         from neq obtain bb: "0 < b * b" and dd: "0 < d * d" and ff: "0 < f * f"
-          by (auto simp add: int_less_le)
+          by (auto simp add: zero_less_mult_iff linorder_neq_iff)
         have "(a * d) * (b * d) * (f * f) \<le> (c * b) * (b * d) * (f * f)"
         proof -
           from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)"
             by (simp add: le_rat)
-          with ff show ?thesis by (simp add: zmult_zle_cancel2)
+          with ff show ?thesis by (simp add: mult_le_cancel_right)
         qed
         also have "... = (c * f) * (d * f) * (b * b)"
-          by (simp only: zmult_ac)
+          by (simp only: mult_ac)
         also have "... \<le> (e * d) * (d * f) * (b * b)"
         proof -
           from neq 2 have "(c * f) * (d * f) \<le> (e * d) * (d * f)"
             by (simp add: le_rat)
-          with bb show ?thesis by (simp add: zmult_zle_cancel2)
+          with bb show ?thesis by (simp add: mult_le_cancel_right)
         qed
         finally have "(a * f) * (b * f) * (d * d) \<le> e * b * (b * f) * (d * d)"
-          by (simp only: zmult_ac)
+          by (simp only: mult_ac)
         with dd have "(a * f) * (b * f) \<le> (e * b) * (b * f)"
-          by (simp add: zmult_zle_cancel2)
+          by (simp add: mult_le_cancel_right)
         with neq show ?thesis by (simp add: le_rat)
       qed
     qed
@@ -570,7 +571,7 @@
         proof -
           from neq 2 have "(c * b) * (d * b) \<le> (a * d) * (d * b)"
             by (simp add: le_rat)
-          thus ?thesis by (simp only: zmult_ac)
+          thus ?thesis by (simp only: mult_ac)
         qed
         finally have "(a * d) * (b * d) = (c * b) * (b * d)" .
         moreover from neq have "b * d \<noteq> 0" by simp
@@ -584,7 +585,7 @@
     show "(q < r) = (q \<le> r \<and> q \<noteq> r)"
       by (simp only: less_rat_def)
     show "q \<le> r \<or> r \<le> q"
-      by (induct q, induct r) (simp add: le_rat zmult_ac, arith)
+      by (induct q, induct r) (simp add: le_rat mult_ac, arith)
   }
 qed
 
@@ -601,12 +602,12 @@
     show "Fract e f + Fract a b \<le> Fract e f + Fract c d"
     proof -
       let ?F = "f * f" from neq have F: "0 < ?F"
-        by (auto simp add: int_less_le)
+        by (auto simp add: zero_less_mult_iff)
       from neq le have "(a * d) * (b * d) \<le> (c * b) * (b * d)"
         by (simp add: le_rat)
       with F have "(a * d) * (b * d) * ?F * ?F \<le> (c * b) * (b * d) * ?F * ?F"
-        by (simp add: zmult_zle_cancel2)
-      with neq show ?thesis by (simp add: add_rat le_rat zmult_ac int_distrib)
+        by (simp add: mult_le_cancel_right)
+      with neq show ?thesis by (simp add: add_rat le_rat mult_ac int_distrib)
     qed
   qed
   show "q < r ==> 0 < s ==> s * q < s * r"
@@ -621,13 +622,13 @@
       from neq gt have "0 < ?E"
         by (auto simp add: zero_rat less_rat le_rat int_less_le eq_rat)
       moreover from neq have "0 < ?F"
-        by (auto simp add: int_less_le)
+        by (auto simp add: zero_less_mult_iff)
       moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)"
         by (simp add: less_rat)
       ultimately have "(a * d) * (b * d) * ?E * ?F < (c * b) * (b * d) * ?E * ?F"
-        by (simp add: zmult_zless_cancel2)
+        by (simp add: mult_less_cancel_right)
       with neq show ?thesis
-        by (simp add: less_rat mult_rat zmult_ac)
+        by (simp add: less_rat mult_rat mult_ac)
     qed
   qed
   show "\<bar>q\<bar> = (if q < 0 then -q else q)"