# HG changeset patch
# User haftmann
# Date 1424296008 -3600
# Node ID 05573e5504a93023175081e18355817e70d43ae7
# Parent  4044f53326c9ee76650e7d2dfea90dc9658b4e20
eliminated fact duplicates

diff -r 4044f53326c9 -r 05573e5504a9 NEWS
--- a/NEWS	Wed Feb 18 22:46:47 2015 +0100
+++ b/NEWS	Wed Feb 18 22:46:48 2015 +0100
@@ -68,6 +68,11 @@
 
 *** HOL ***
 
+* Eliminated fact duplicates:
+  mult_less_imp_less_right ~> mult_right_less_imp_less
+  mult_less_imp_less_left ~> mult_left_less_imp_less
+Minor INCOMPATIBILITY.
+
 * Fact consolidation: even_less_0_iff is subsumed by
 double_add_less_zero_iff_single_add_less_zero (simp by default anyway).
 
diff -r 4044f53326c9 -r 05573e5504a9 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Feb 18 22:46:47 2015 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Feb 18 22:46:48 2015 +0100
@@ -217,7 +217,7 @@
       using b v
       apply (simp add: th2)
       done
-    from mult_less_imp_less_left[OF th4 th3]
+    from mult_left_less_imp_less[OF th4 th3]
     have "?P ?w n" unfolding th1 .
     then have "\<exists>z. ?P z n" ..
   }
diff -r 4044f53326c9 -r 05573e5504a9 src/HOL/Multivariate_Analysis/Fashoda.thy
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Wed Feb 18 22:46:47 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Wed Feb 18 22:46:48 2015 +0100
@@ -590,7 +590,7 @@
       then have "(1 - u) * b > (1 - u) * a"
         by (auto simp add:field_simps)
       then have "b \<ge> a"
-        apply (drule_tac mult_less_imp_less_left)
+        apply (drule_tac mult_left_less_imp_less)
         using u
         apply auto
         done
@@ -607,7 +607,7 @@
       then have "(1 - u) * a \<le> (1 - u) * b"
         apply -
         apply (rule mult_left_mono)
-        apply (drule mult_less_imp_less_left)
+        apply (drule mult_left_less_imp_less)
         using u
         apply auto
         done
@@ -671,7 +671,7 @@
       then have "(1 - u) * b > (1 - u) * a"
         by (auto simp add: field_simps)
       then have "b \<ge> a"
-        apply (drule_tac mult_less_imp_less_left)
+        apply (drule_tac mult_left_less_imp_less)
         using u
         apply auto
         done
@@ -688,7 +688,7 @@
       then have "(1 - u) * a \<le> (1 - u) * b"
         apply -
         apply (rule mult_left_mono)
-        apply (drule mult_less_imp_less_left)
+        apply (drule mult_left_less_imp_less)
         using u
         apply auto
         done
diff -r 4044f53326c9 -r 05573e5504a9 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Wed Feb 18 22:46:47 2015 +0100
+++ b/src/HOL/Rings.thy	Wed Feb 18 22:46:48 2015 +0100
@@ -718,16 +718,6 @@
   apply simp
   done
 
-lemma mult_less_imp_less_left:
-  assumes "c * a < c * b" and "0 \<le> c"
-  shows "a < b"
-  using assms by (fact mult_left_less_imp_less)
-
-lemma mult_less_imp_less_right:
-  assumes less: "a * c < b * c" and nonneg: "0 \<le> c"
-  shows "a < b"
-  using assms by (fact mult_right_less_imp_less)
-
 end
 
 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1