# HG changeset patch
# User haftmann
# Date 1268916994 -3600
# Node ID bd26885af9f41e1b7bcb0416b6e7d69053491463
# Parent  67e4de90d2c28fe0b59116ac694902723068c9ec
dropped odd interpretation of comm_monoid_mult into comm_monoid_add

diff -r 67e4de90d2c2 -r bd26885af9f4 src/HOL/SupInf.thy
--- a/src/HOL/SupInf.thy	Thu Mar 18 13:56:34 2010 +0100
+++ b/src/HOL/SupInf.thy	Thu Mar 18 13:56:34 2010 +0100
@@ -355,13 +355,13 @@
 
 lemma Inf_greater:
   fixes z :: real
-  shows "X \<noteq> {} \<Longrightarrow>  Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
+  shows "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
   by (metis Inf_real_iff mem_def not_leE)
 
 lemma Inf_close:
   fixes e :: real
   shows "X \<noteq> {} \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>x \<in> X. x < Inf X + e"
-  by (metis add_strict_increasing comm_monoid_add.mult_commute Inf_greater linorder_not_le pos_add_strict)
+  by (metis add_strict_increasing add_commute Inf_greater linorder_not_le pos_add_strict)
 
 lemma Inf_finite_Min:
   fixes S :: "real set"
@@ -417,7 +417,7 @@
   also have "... \<le> e" 
     apply (rule Sup_asclose) 
     apply (auto simp add: S)
-    apply (metis abs_minus_add_cancel b comm_monoid_add.mult_commute real_diff_def) 
+    apply (metis abs_minus_add_cancel b add_commute real_diff_def) 
     done
   finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
   thus ?thesis