Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Decision_Procs/MIR.thy
changeset 36778 739a9379e29b
parent 36531 19f6e3b0d9b6
child 36870 b897bd9ca71b 
--- a/src/HOL/Decision_Procs/MIR.thy	Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Decision_Procs/MIR.thy	Sun May 09 22:51:11 2010 -0700
@@ -2177,7 +2177,7 @@
     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
     hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
-      by (simp only:  real_mult_less_mono2[OF rcpos th1])
+      by (simp only: mult_strict_left_mono [OF th1 rcpos])
     hence "real c * real x + Inum (y # bs) e \<noteq> 0"using rcpos  by simp
     thus "real c * real x + Inum (real x # bs) e \<noteq> 0" 
       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"]  by simp
@@ -2194,7 +2194,7 @@
     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
     hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
-      by (simp only:  real_mult_less_mono2[OF rcpos th1])
+      by (simp only: mult_strict_left_mono [OF th1 rcpos])
     hence "real c * real x + Inum (y # bs) e \<noteq> 0"using rcpos  by simp
     thus "real c * real x + Inum (real x # bs) e \<noteq> 0" 
       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"]  by simp
@@ -2211,7 +2211,7 @@
     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
     hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
-      by (simp only:  real_mult_less_mono2[OF rcpos th1])
+      by (simp only: mult_strict_left_mono [OF th1 rcpos])
     thus "real c * real x + Inum (real x # bs) e < 0" 
       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
   qed
@@ -2227,7 +2227,7 @@
     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
     hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
-      by (simp only:  real_mult_less_mono2[OF rcpos th1])
+      by (simp only: mult_strict_left_mono [OF th1 rcpos])
     thus "real c * real x + Inum (real x # bs) e \<le> 0" 
       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
   qed
@@ -2243,7 +2243,7 @@
     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
     hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
-      by (simp only:  real_mult_less_mono2[OF rcpos th1])
+      by (simp only: mult_strict_left_mono [OF th1 rcpos])
     thus "\<not> (real c * real x + Inum (real x # bs) e>0)" 
       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
   qed
@@ -2259,7 +2259,7 @@
     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
     hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
-      by (simp only:  real_mult_less_mono2[OF rcpos th1])
+      by (simp only: mult_strict_left_mono [OF th1 rcpos])
     thus "\<not> real c * real x + Inum (real x # bs) e \<ge> 0" 
       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
   qed
isabelle