# HG changeset patch
# User haftmann
# Date 1387989546 -3600
# Node ID 82acc20ded73cbb8386f71bc7a9f3072684aa86c
# Parent  c65e5cbdbc9703e996ad25a0481d4bc616394ecb
prefer more canonical names for lemmas on min/max

diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -1252,7 +1252,7 @@
           h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<oplus>\<^bsub>S\<^esub>
         (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q} \<union> {deg R q<..max (deg R p) (deg R q)}.
           h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
-      by (simp only: ivl_disj_un_one le_maxI1 le_maxI2)
+      by (simp only: ivl_disj_un_one max.cobounded1 max.cobounded2)
     also from R S have "... =
       (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<oplus>\<^bsub>S\<^esub>
       (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Bali/Evaln.thy
--- a/src/HOL/Bali/Evaln.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Bali/Evaln.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -459,7 +459,7 @@
 
 lemma evaln_max2: "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2')\<rbrakk> \<Longrightarrow> 
              G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> (w1, s1') \<and> G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> (w2, s2')"
-by (fast intro: le_maxI1 le_maxI2)
+by (fast intro: max.cobounded1 max.cobounded2)
 
 corollary evaln_max2E [consumes 2]:
   "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); 
@@ -473,7 +473,7 @@
  G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w2, s2') \<and> 
  G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w3, s3')"
 apply (drule (1) evaln_max2, erule thin_rl)
-apply (fast intro!: le_maxI1 le_maxI2)
+apply (fast intro!: max.cobounded1 max.cobounded2)
 done
 
 corollary evaln_max3E: 
@@ -489,10 +489,10 @@
 lemma le_max3I1: "(n2::nat) \<le> max n1 (max n2 n3)"
 proof -
   have "n2 \<le> max n2 n3"
-    by (rule le_maxI1)
+    by (rule max.cobounded1)
   also
   have "max n2 n3 \<le> max n1 (max n2 n3)"
-    by (rule le_maxI2)
+    by (rule max.cobounded2)
   finally
   show ?thesis .
 qed
@@ -500,10 +500,10 @@
 lemma le_max3I2: "(n3::nat) \<le> max n1 (max n2 n3)"
 proof -
   have "n3 \<le> max n2 n3"
-    by (rule le_maxI2)
+    by (rule max.cobounded2)
   also
   have "max n2 n3 \<le> max n1 (max n2 n3)"
-    by (rule le_maxI2)
+    by (rule max.cobounded2)
   finally
   show ?thesis .
 qed
@@ -568,13 +568,13 @@
         then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and> 
               G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3)
         else s3 = s1"
-    by simp (iprover intro: evaln_nonstrict le_maxI1 le_maxI2)
+    by simp (iprover intro: evaln_nonstrict max.cobounded1 max.cobounded2)
   ultimately
   have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3"
     apply -
     apply (rule evaln.Loop)
-    apply   (iprover intro: evaln_nonstrict intro: le_maxI1)
-    apply   (auto intro: evaln_nonstrict intro: le_maxI2)
+    apply   (iprover intro: evaln_nonstrict intro: max.cobounded1)
+    apply   (auto intro: evaln_nonstrict intro: max.cobounded2)
     done
   then show ?case ..
 next
@@ -603,7 +603,7 @@
     by fastforce 
   ultimately
   have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2\<rightarrow> s3"
-    by (auto intro!: evaln.Try le_maxI1 le_maxI2)
+    by (auto intro!: evaln.Try max.cobounded1 max.cobounded2)
   then show ?case ..
 next
   case (Fin s0 c1 x1 s1 c2 s2 s3)
@@ -629,7 +629,7 @@
               \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
                    G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
                    s3 = restore_lvars s1 s2)"
-    by (auto intro: evaln_nonstrict le_maxI1 le_maxI2)
+    by (auto intro: evaln_nonstrict max.cobounded1 max.cobounded2)
   ultimately have "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
     by (rule evaln.Init)
   then show ?case ..
@@ -755,7 +755,7 @@
   ultimately
   have "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
             (set_lvars (locals (store s2))) s4"
-    by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
+    by (auto intro!: evaln.Call max.cobounded1 le_max3I1 le_max3I2)
   thus ?case ..
 next
   case (Methd s0 D sig v s1)
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -444,7 +444,7 @@
   assumes g0: "numgcd t = 0"
   shows "Inum bs t = 0"
   using g0[simplified numgcd_def] 
-  by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos min_max.sup_absorb2)
+  by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos max.absorb2)
 
 lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"
   using gp
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/HOLCF/Completion.thy
--- a/src/HOL/HOLCF/Completion.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/HOLCF/Completion.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -62,8 +62,8 @@
  apply (rule idealI)
    apply (cut_tac idealD1 [OF ideal_A], fast)
   apply (clarify, rename_tac i j)
-  apply (drule subsetD [OF chain_A [OF le_maxI1]])
-  apply (drule subsetD [OF chain_A [OF le_maxI2]])
+  apply (drule subsetD [OF chain_A [OF max.cobounded1]])
+  apply (drule subsetD [OF chain_A [OF max.cobounded2]])
   apply (drule (1) idealD2 [OF ideal_A])
   apply blast
  apply clarify
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/HOLCF/Library/List_Cpo.thy
--- a/src/HOL/HOLCF/Library/List_Cpo.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/HOLCF/Library/List_Cpo.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -273,8 +273,8 @@
 apply (erule list_chain_cases)
 apply (auto simp add: lub_Cons dest!: compactD2)
 apply (rename_tac i j, rule_tac x="max i j" in exI)
-apply (drule (1) below_trans [OF _ chain_mono [OF _ le_maxI1]])
-apply (drule (1) below_trans [OF _ chain_mono [OF _ le_maxI2]])
+apply (drule (1) below_trans [OF _ chain_mono [OF _ max.cobounded1]])
+apply (drule (1) below_trans [OF _ chain_mono [OF _ max.cobounded2]])
 apply (erule (1) conjI)
 done
 
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/HOLCF/Pcpo.thy
--- a/src/HOL/HOLCF/Pcpo.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/HOLCF/Pcpo.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -118,8 +118,8 @@
     apply (rule lub_below [OF 2])
     apply (rule below_lub [OF 3])
     apply (rule below_trans)
-    apply (rule chain_mono [OF 1 le_maxI1])
-    apply (rule chain_mono [OF 2 le_maxI2])
+    apply (rule chain_mono [OF 1 max.cobounded1])
+    apply (rule chain_mono [OF 2 max.cobounded2])
     done
   show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)"
     apply (rule lub_mono [OF 3 4])
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/HOLCF/Universal.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -802,7 +802,7 @@
       by (simp add: approximants_def approx_below)
     moreover from x y have "x \<sqsubseteq> ?z \<and> y \<sqsubseteq> ?z"
       by (simp add: approximants_def compact_le_def)
-         (metis i j monofun_cfun chain_mono chain_approx le_maxI1 le_maxI2)
+         (metis i j monofun_cfun chain_mono chain_approx max.cobounded1 max.cobounded2)
     ultimately show "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" ..
   next
     fix x y :: "'a compact_basis"
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Hoare_Parallel/Graph.thy
--- a/src/HOL/Hoare_Parallel/Graph.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Hoare_Parallel/Graph.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -182,7 +182,7 @@
 
 subsubsection{* Graph 3 *}
 
-declare min_max.inf_absorb1 [simp] min_max.inf_absorb2 [simp]
+declare min.absorb1 [simp] min.absorb2 [simp]
 
 lemma Graph3: 
   "\<lbrakk> T\<in>Reach E; R<length E \<rbrakk> \<Longrightarrow> Reach(E[R:=(fst(E!R),T)]) \<subseteq> Reach E"
@@ -304,7 +304,7 @@
 apply force
 done
 
-declare min_max.inf_absorb1 [simp del] min_max.inf_absorb2 [simp del]
+declare min.absorb1 [simp del] min.absorb2 [simp del]
 
 subsubsection {* Graph 5 *}
 
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/IMP/Sec_Typing.thy
--- a/src/HOL/IMP/Sec_Typing.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/IMP/Sec_Typing.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -48,19 +48,19 @@
 next
   case (IfTrue b s c1)
   hence "max (sec b) l \<turnstile> c1" by auto
-  hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
+  hence "l \<turnstile> c1" by (metis max.cobounded2 anti_mono)
   thus ?case using IfTrue.IH by metis
 next
   case (IfFalse b s c2)
   hence "max (sec b) l \<turnstile> c2" by auto
-  hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
+  hence "l \<turnstile> c2" by (metis max.cobounded2 anti_mono)
   thus ?case using IfFalse.IH by metis
 next
   case WhileFalse thus ?case by auto
 next
   case (WhileTrue b s1 c)
   hence "max (sec b) l \<turnstile> c" by auto
-  hence "l \<turnstile> c" by (metis le_maxI2 anti_mono)
+  hence "l \<turnstile> c" by (metis max.cobounded2 anti_mono)
   thus ?case using WhileTrue by metis
 qed
 
@@ -200,8 +200,8 @@
 apply (metis Skip')
 apply (metis Assign')
 apply (metis Seq')
-apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono')
-by (metis less_or_eq_imp_le min_max.sup_absorb1 min_max.sup_absorb2 nat_le_linear While' anti_mono')
+apply (metis min_max.inf_sup_ord(3) max.absorb2 nat_le_linear If' anti_mono')
+by (metis less_or_eq_imp_le max.absorb1 max.absorb2 nat_le_linear While' anti_mono')
 
 
 lemma sec_type'_sec_type: "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
@@ -209,8 +209,8 @@
 apply (metis Skip)
 apply (metis Assign)
 apply (metis Seq)
-apply (metis min_max.sup_absorb2 If)
-apply (metis min_max.sup_absorb2 While)
+apply (metis max.absorb2 If)
+apply (metis max.absorb2 While)
 by (metis anti_mono)
 
 subsection "A Bottom-Up Typing System"
@@ -233,15 +233,15 @@
 apply(induction rule: sec_type2.induct)
 apply (metis Skip')
 apply (metis Assign' eq_imp_le)
-apply (metis Seq' anti_mono' min_max.inf_le1 min_max.inf_le2)
-apply (metis If' anti_mono' min_max.inf_absorb2 min_max.le_iff_inf nat_le_linear)
+apply (metis Seq' anti_mono' min.cobounded1 min.cobounded2)
+apply (metis If' anti_mono' min.absorb2 min.absorb_iff1 nat_le_linear)
 by (metis While')
 
 lemma sec_type'_sec_type2: "l \<turnstile>' c \<Longrightarrow> \<exists> l' \<ge> l. \<turnstile> c : l'"
 apply(induction rule: sec_type'.induct)
 apply (metis Skip2 le_refl)
 apply (metis Assign2)
-apply (metis Seq2 min_max.inf_greatest)
+apply (metis Seq2 min.boundedI)
 apply (metis If2 inf_greatest inf_nat_def le_trans)
 apply (metis While2 le_trans)
 by (metis le_trans)
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/IMP/Sec_TypingT.thy
--- a/src/HOL/IMP/Sec_TypingT.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/IMP/Sec_TypingT.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -41,12 +41,12 @@
 next
   case (IfTrue b s c1)
   hence "max (sec b) l \<turnstile> c1" by auto
-  hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
+  hence "l \<turnstile> c1" by (metis max.cobounded2 anti_mono)
   thus ?case using IfTrue.IH by metis
 next
   case (IfFalse b s c2)
   hence "max (sec b) l \<turnstile> c2" by auto
-  hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
+  hence "l \<turnstile> c2" by (metis max.cobounded2 anti_mono)
   thus ?case using IfFalse.IH by metis
 next
   case WhileFalse thus ?case by auto
@@ -61,7 +61,7 @@
 apply (metis big_step.Skip)
 apply (metis big_step.Assign)
 apply (metis big_step.Seq)
-apply (metis IfFalse IfTrue le0 le_antisym le_maxI2)
+apply (metis IfFalse IfTrue le0 le_antisym max.cobounded2)
 apply simp
 done
 
@@ -190,7 +190,7 @@
 apply (metis Skip')
 apply (metis Assign')
 apply (metis Seq')
-apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono')
+apply (metis min_max.inf_sup_ord(3) max.absorb2 nat_le_linear If' anti_mono')
 by (metis While')
 
 
@@ -200,7 +200,7 @@
 apply (metis Skip)
 apply (metis Assign)
 apply (metis Seq)
-apply (metis min_max.sup_absorb2 If)
+apply (metis max.absorb2 If)
 apply (metis While)
 by (metis anti_mono)
 
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Import/HOL_Light_Maps.thy
--- a/src/HOL/Import/HOL_Light_Maps.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Import/HOL_Light_Maps.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -175,11 +175,11 @@
 
 lemma DEF_MAX[import_const "MAX"]:
   "max = (\<lambda>x y :: nat. if x \<le> y then y else x)"
-  by (auto simp add: min_max.le_iff_sup fun_eq_iff)
+  by (auto simp add: max.absorb_iff2 fun_eq_iff)
 
 lemma DEF_MIN[import_const "MIN"]:
   "min = (\<lambda>x y :: nat. if x \<le> y then x else y)"
-  by (auto simp add: min_max.le_iff_inf fun_eq_iff)
+  by (auto simp add: min.absorb_iff1 fun_eq_iff)
 
 lemma EVEN[import_const "EVEN" : "Parity.even_odd_class.even"]:
   "even (id 0\<Colon>nat) = True \<and> (\<forall>n. even (Suc n) = (\<not> even n))"
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Int.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -114,7 +114,7 @@
 
 instance
   by intro_classes
-    (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
+    (auto simp add: inf_int_def sup_int_def max_min_distrib2)
 
 end
 
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Lattices_Big.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -371,10 +371,10 @@
     by (simp only: min_max.Sup_fin_def Max_def)
 qed
 
-lemmas le_maxI1 = min_max.sup_ge1
-lemmas le_maxI2 = min_max.sup_ge2
-lemmas min_ac = min.assoc min_max.inf_commute min.left_commute
-lemmas max_ac = min_max.sup_assoc min_max.sup_commute max.left_commute
+lemmas le_maxI1 = max.cobounded1
+lemmas le_maxI2 = max.cobounded2
+lemmas min_ac = min.assoc min.commute min.left_commute
+lemmas max_ac = max.assoc max.commute max.left_commute
 
 end
 
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Library/BigO.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -171,7 +171,7 @@
   apply (subgoal_tac "c <= max c ca")
   apply (erule order_less_le_trans)
   apply assumption
-  apply (rule le_maxI1)
+  apply (rule max.cobounded1)
   apply clarify
   apply (drule_tac x = "xa" in spec)+
   apply (subgoal_tac "0 <= f xa + g xa")
@@ -184,12 +184,12 @@
   apply (subgoal_tac "c * f xa <= max c ca * f xa")
   apply (force)
   apply (rule mult_right_mono)
-  apply (rule le_maxI1)
+  apply (rule max.cobounded1)
   apply assumption
   apply (subgoal_tac "ca * g xa <= max c ca * g xa")
   apply (force)
   apply (rule mult_right_mono)
-  apply (rule le_maxI2)
+  apply (rule max.cobounded2)
   apply assumption
   apply (rule abs_triangle_ineq)
   apply (rule add_nonneg_nonneg)
@@ -770,7 +770,7 @@
   apply (rule bigo_lesseq4)
   apply (erule set_plus_imp_minus)
   apply (rule allI)
-  apply (rule le_maxI2)
+  apply (rule max.cobounded2)
   apply (rule allI)
   apply (subst fun_diff_def)
   apply (case_tac "0 <= k x - g x")
@@ -794,7 +794,7 @@
   apply (rule bigo_lesseq4)
   apply (erule set_plus_imp_minus)
   apply (rule allI)
-  apply (rule le_maxI2)
+  apply (rule max.cobounded2)
   apply (rule allI)
   apply (subst fun_diff_def)
   apply (case_tac "0 <= f x - k x")
@@ -836,7 +836,7 @@
   apply (subgoal_tac "abs(max (f x - g x) 0) = max (f x - g x) 0")
   apply (clarsimp simp add: algebra_simps) 
   apply (rule abs_of_nonneg)
-  apply (rule le_maxI2)
+  apply (rule max.cobounded2)
   done
 
 lemma lesso_add: "f <o g =o O(h) ==>
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Library/Char_ord.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -32,7 +32,7 @@
   "(sup \<Colon> nibble \<Rightarrow> _) = max"
 
 instance proof
-qed (auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
+qed (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2)
 
 end
 
@@ -90,7 +90,7 @@
   "(sup \<Colon> char \<Rightarrow> _) = max"
 
 instance proof
-qed (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1)
+qed (auto simp add: inf_char_def sup_char_def max_min_distrib2)
 
 end
 
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -1622,7 +1622,7 @@
         then have "range f = {0}"
           by auto
         with True show "c * SUPR UNIV f \<le> y"
-          using * by (auto simp: SUP_def min_max.sup_absorb1)
+          using * by (auto simp: SUP_def max.absorb1)
       next
         case False
         then obtain i where "f i \<noteq> 0"
@@ -1779,7 +1779,7 @@
   proof (cases a)
     case PInf with `A \<noteq> {}`
     show ?thesis
-      by (auto simp: image_constant min_max.sup_absorb1)
+      by (auto simp: image_constant max.absorb1)
   next
     case (real r)
     then have **: "op + (- a) ` op + a ` A = A"
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Library/Fraction_Field.thy
--- a/src/HOL/Library/Fraction_Field.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Library/Fraction_Field.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -424,7 +424,7 @@
 instance
   by intro_classes
     (auto simp add: abs_fract_def sgn_fract_def
-      min_max.sup_inf_distrib1 inf_fract_def sup_fract_def)
+      max_min_distrib2 inf_fract_def sup_fract_def)
 
 end
 
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Library/Lattice_Algebras.thy
--- a/src/HOL/Library/Lattice_Algebras.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Library/Lattice_Algebras.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -384,7 +384,7 @@
 proof -
   note add_le_cancel_right [of a a "- a", symmetric, simplified]
   moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified]
-  then show ?thesis by (auto simp: sup_max min_max.sup_absorb1 min_max.sup_absorb2)
+  then show ?thesis by (auto simp: sup_max max.absorb1 max.absorb2)
 qed
 
 lemma abs_if_lattice:
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Library/List_lexord.thy
--- a/src/HOL/Library/List_lexord.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Library/List_lexord.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -74,7 +74,7 @@
 definition "(sup \<Colon> 'a list \<Rightarrow> _) = max"
 
 instance
-  by default (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
+  by default (auto simp add: inf_list_def sup_list_def max_min_distrib2)
 
 end
 
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Library/Product_Lexorder.thy
--- a/src/HOL/Library/Product_Lexorder.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Library/Product_Lexorder.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -55,7 +55,7 @@
   "(sup :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
 
 instance
-  by default (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
+  by default (auto simp add: inf_prod_def sup_prod_def max_min_distrib2)
 
 end
 
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Library/Saturated.thy
--- a/src/HOL/Library/Saturated.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Library/Saturated.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -41,7 +41,7 @@
 
 lemma min_len_of_nat_of [simp]:
   "min (len_of TYPE('a)) (nat_of (n::('a::len) sat)) = nat_of n"
-  by (rule min_max.inf_absorb2 [OF nat_of_le_len_of])
+  by (rule min.absorb2 [OF nat_of_le_len_of])
 
 lemma min_nat_of_len_of [simp]:
   "min (nat_of (n::('a::len) sat)) (len_of TYPE('a)) = nat_of n"
@@ -61,7 +61,7 @@
   less_sat_def: "x < y \<longleftrightarrow> nat_of x < nat_of y"
 
 instance
-by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min_max.le_infI1 nat_mult_commute)
+by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 nat_mult_commute)
 
 end
 
@@ -117,14 +117,14 @@
       case True thus ?thesis by (simp add: sat_eq_iff)
     next
       case False with `a \<noteq> 0` show ?thesis
-        by (simp add: sat_eq_iff nat_mult_min_left nat_mult_min_right mult_assoc min_max.inf_assoc min_max.inf_absorb2)
+        by (simp add: sat_eq_iff nat_mult_min_left nat_mult_min_right mult_assoc min.assoc min.absorb2)
     qed
   qed
 next
   fix a :: "('a::len) sat"
   show "1 * a = a"
     apply (simp add: sat_eq_iff)
-    apply (metis One_nat_def len_gt_0 less_Suc0 less_zeroE linorder_not_less min_max.le_iff_inf min_nat_of_len_of nat_mult_1_right nat_mult_commute)
+    apply (metis One_nat_def len_gt_0 less_Suc0 less_zeroE linorder_not_less min.absorb_iff1 min_nat_of_len_of nat_mult_1_right nat_mult_commute)
     done
 next
   fix a b c :: "('a::len) sat"
@@ -133,7 +133,7 @@
     case True thus ?thesis by (simp add: sat_eq_iff)
   next
     case False thus ?thesis
-      by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib min_add_distrib_left min_add_distrib_right min_max.inf_assoc min_max.inf_absorb2)
+      by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib min_add_distrib_left min_add_distrib_right min.assoc min.absorb2)
   qed
 qed (simp_all add: sat_eq_iff mult.commute)
 
@@ -143,7 +143,7 @@
 begin
 
 instance
-by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min_max.le_infI1 nat_mult_commute)
+by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 nat_mult_commute)
 
 end
 
@@ -202,7 +202,7 @@
   "top = Sat (len_of TYPE('a))"
 
 instance proof
-qed (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def min_max.sup_inf_distrib1,
+qed (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def max_min_distrib2,
   simp_all add: less_eq_sat_def)
 
 end
@@ -243,7 +243,7 @@
   note finite
   moreover assume "x \<in> A"
   ultimately show "Inf A \<le> x"
-    by (induct A) (auto intro: min_max.le_infI2)
+    by (induct A) (auto intro: min.coboundedI2)
 next
   fix z :: "'a sat"
   fix A :: "'a sat set"
@@ -256,7 +256,7 @@
   note finite
   moreover assume "x \<in> A"
   ultimately show "x \<le> Sup A"
-    by (induct A) (auto intro: min_max.le_supI2)
+    by (induct A) (auto intro: max.coboundedI2)
 next
   fix z :: "'a sat"
   fix A :: "'a sat set"
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Limits.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -125,7 +125,7 @@
 proof safe
   fix N K assume "0 < K" "\<forall>n\<ge>N. norm (X n) \<le> K"
   then show "\<exists>K>0. \<forall>n. norm (X n) \<le> K"
-    by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] min_max.less_supI2)
+    by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] max.strict_coboundedI2)
        (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj)
 qed auto
 
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/List.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -2065,13 +2065,13 @@
 
 lemma butlast_take:
   "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
-by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)
+by (simp add: butlast_conv_take min.absorb1 min.absorb2)
 
 lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
 by (simp add: butlast_conv_take drop_take add_ac)
 
 lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
-by (simp add: butlast_conv_take min_max.inf_absorb1)
+by (simp add: butlast_conv_take min.absorb1)
 
 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
 by (simp add: butlast_conv_take drop_take add_ac)
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Metis_Examples/Big_O.thy
--- a/src/HOL/Metis_Examples/Big_O.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -212,8 +212,8 @@
   apply (metis abs_triangle_ineq)
  apply (metis add_nonneg_nonneg)
 apply (rule add_mono)
- apply (metis le_maxI2 linorder_linear min_max.sup_absorb1 mult_right_mono xt1(6))
-by (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
+ apply (metis max.cobounded2 linorder_linear max.absorb1 mult_right_mono xt1(6))
+by (metis max.cobounded2 linorder_not_le mult_le_cancel_right order_trans)
 
 lemma bigo_bounded_alt: "\<forall>x. 0 <= f x \<Longrightarrow> \<forall>x. f x <= c * g x \<Longrightarrow> f : O(g)"
 apply (auto simp add: bigo_def)
@@ -658,7 +658,7 @@
 apply (subgoal_tac "(\<lambda>x. max (f x - g x) 0) = 0")
  apply (metis bigo_zero)
 by (metis (lifting, no_types) func_zero le_fun_def le_iff_diff_le_0
-      min_max.sup_absorb2 order_eq_iff)
+      max.absorb2 order_eq_iff)
 
 lemma bigo_lesso2: "f =o g +o O(h) \<Longrightarrow>
     \<forall>x. 0 <= k x \<Longrightarrow> \<forall>x. k x <= f x \<Longrightarrow>
@@ -667,15 +667,15 @@
   apply (rule bigo_lesseq4)
   apply (erule set_plus_imp_minus)
   apply (rule allI)
-  apply (rule le_maxI2)
+  apply (rule max.cobounded2)
   apply (rule allI)
   apply (subst fun_diff_def)
 apply (erule thin_rl)
 (* sledgehammer *)
 apply (case_tac "0 <= k x - g x")
  apply (metis (lifting) abs_le_D1 linorder_linear min_diff_distrib_left
-          min_max.inf_absorb1 min_max.inf_absorb2 min_max.sup_absorb1)
-by (metis abs_ge_zero le_cases min_max.sup_absorb2)
+          min.absorb1 min.absorb2 max.absorb1)
+by (metis abs_ge_zero le_cases max.absorb2)
 
 lemma bigo_lesso3: "f =o g +o O(h) \<Longrightarrow>
     \<forall>x. 0 <= k x \<Longrightarrow> \<forall>x. g x <= k x \<Longrightarrow>
@@ -684,7 +684,7 @@
 apply (rule bigo_lesseq4)
   apply (erule set_plus_imp_minus)
  apply (rule allI)
- apply (rule le_maxI2)
+ apply (rule max.cobounded2)
 apply (rule allI)
 apply (subst fun_diff_def)
 apply (erule thin_rl)
@@ -695,7 +695,7 @@
   apply (drule_tac x = x in spec) back
   apply (metis diff_less_0_iff_less linorder_not_le not_leE xt1(12) xt1(6))
  apply (metis add_minus_cancel diff_le_eq le_diff_eq uminus_add_conv_diff)
-by (metis abs_ge_zero linorder_linear min_max.sup_absorb1 min_max.sup_commute)
+by (metis abs_ge_zero linorder_linear max.absorb1 max.commute)
 
 lemma bigo_lesso4:
   "f <o g =o O(k\<Colon>'a=>'b\<Colon>{linordered_field}) \<Longrightarrow>
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -379,7 +379,7 @@
   with Pair 
   have "?app s \<Longrightarrow> ?P s" by (simp only:)
   moreover
-  have "?P s \<Longrightarrow> ?app s" by (clarsimp simp add: min_max.inf_absorb2)
+  have "?P s \<Longrightarrow> ?app s" by (clarsimp simp add: min.absorb2)
   ultimately
   show ?thesis by (rule iffI) 
 qed 
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -442,7 +442,7 @@
 (********************************************************************************)
 
 lemma max_of_list_elem: "x \<in> set xs \<Longrightarrow> x \<le> (max_of_list xs)"
-by (induct xs, auto intro: le_maxI1 simp: le_max_iff_disj max_of_list_def)
+by (induct xs, auto intro: max.cobounded1 simp: le_max_iff_disj max_of_list_def)
 
 lemma max_of_list_sublist: "set xs \<subseteq> set ys 
   \<Longrightarrow> (max_of_list xs) \<le> (max_of_list ys)"
@@ -1053,7 +1053,7 @@
 lemma bc_mt_corresp_New: "\<lbrakk>is_class cG cname \<rbrakk>
   \<Longrightarrow> bc_mt_corresp [New cname] (pushST [Class cname]) (ST, LT) cG rT mxr (Suc 0)"
 apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
-    max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
+    max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
 apply (intro strip)
 apply (rule conjI)
 apply (rule check_type_mono, assumption, simp)
@@ -1064,7 +1064,7 @@
   bc_mt_corresp [Pop] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
   apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
   apply (simp add: max_ssize_def ssize_sto_def max_of_list_def) 
-  apply (simp add: check_type_simps min_max.sup_absorb1)
+  apply (simp add: check_type_simps max.absorb1)
   apply clarify
   apply (rule_tac x="(length ST)" in exI)
   apply simp+
@@ -1087,7 +1087,7 @@
   \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T]) sttp cG rT mxr (Suc 0)"
 apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
   apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
-              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
+              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1106,7 +1106,7 @@
   \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T']) sttp cG rT mxr (Suc 0)"
 apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
   apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
-              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
+              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1124,7 +1124,7 @@
   \<Longrightarrow> bc_mt_corresp [Load i] 
          (\<lambda>(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)"
 apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
-            max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
+            max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1148,7 +1148,7 @@
   apply (simp add: max_ssize_def  max_of_list_def)
   apply (simp add: ssize_sto_def)
   apply (intro strip)
-apply (simp add: check_type_simps min_max.sup_absorb1)
+apply (simp add: check_type_simps max.absorb1)
 apply clarify
 apply (rule conjI)
 apply (rule_tac x="(length ST)" in exI)
@@ -1162,7 +1162,7 @@
   apply (simp add: sup_state_conv)
   apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
  apply (intro strip)
-apply (simp add: check_type_simps min_max.sup_absorb1)
+apply (simp add: check_type_simps max.absorb1)
 apply clarify
 apply (rule_tac x="(length ST)" in exI)
 apply simp+
@@ -1172,7 +1172,7 @@
 lemma bc_mt_corresp_Dup: "
   bc_mt_corresp [Dup] dupST (T # ST, LT) cG rT mxr (Suc 0)"
  apply (simp add: bc_mt_corresp_def dupST_def wt_instr_altern_def
-             max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
+             max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1185,7 +1185,7 @@
 lemma bc_mt_corresp_Dup_x1: "
   bc_mt_corresp [Dup_x1] dup_x1ST (T1 # T2 # ST, LT) cG rT mxr (Suc 0)"
   apply (simp add: bc_mt_corresp_def dup_x1ST_def wt_instr_altern_def
-              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
+              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1202,7 +1202,7 @@
          (PrimT Integer # PrimT Integer # ST, LT) cG rT mxr (Suc 0)"
   apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
   apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
-  apply (simp add: check_type_simps min_max.sup_absorb1)
+  apply (simp add: check_type_simps max.absorb1)
   apply clarify
   apply (rule_tac x="Suc (length ST)" in exI)
   apply simp+
@@ -1245,7 +1245,7 @@
   apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
 
   apply (intro strip)
-apply (simp add: check_type_simps min_max.sup_absorb1)
+apply (simp add: check_type_simps max.absorb1)
 apply clarify
 apply (rule_tac x="Suc (length ST)" in exI)
 apply simp+
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/MicroJava/DFA/LBVSpec.thy
--- a/src/HOL/MicroJava/DFA/LBVSpec.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/MicroJava/DFA/LBVSpec.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -283,7 +283,7 @@
   shows "wtl (take (pc+1) is) c 0 s = wtc c pc (wtl (take pc is) c 0 s)"
 proof -
   from suc have "take (pc+1) is=(take pc is)@[is!pc]" by (simp add: take_Suc)
-  with suc wtl show ?thesis by (simp add: min_max.inf_absorb2)
+  with suc wtl show ?thesis by (simp add: min.absorb2)
 qed
 
 lemma (in lbv) wtl_all:
@@ -298,7 +298,7 @@
   with all have take: "?wtl (take pc is@i#r) \<noteq> \<top>" by simp 
   from pc have "is!pc = drop pc is ! 0" by simp
   with Cons have "is!pc = i" by simp
-  with take pc show ?thesis by (auto simp add: min_max.inf_absorb2)
+  with take pc show ?thesis by (auto simp add: min.absorb2)
 qed
 
 section "preserves-type"
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -2723,7 +2723,7 @@
     show ?case
       apply (rule_tac x="max B1 B2" in exI)
       apply rule
-      apply (rule min_max.less_supI1)
+      apply (rule max.strict_coboundedI1)
       apply (rule B1)
       apply rule
       apply rule
@@ -9576,7 +9576,7 @@
     show ?case
       apply (rule_tac x="max B1 B2" in exI)
       apply safe
-      apply (rule min_max.less_supI1)
+      apply (rule max.strict_coboundedI1)
       apply (rule B1)
     proof -
       fix a b c d :: 'n
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -2527,7 +2527,7 @@
   apply (drule (1) bspec)
   apply simp
   apply (drule (1) bspec)
-  apply (rule min_max.le_supI2)
+  apply (rule max.coboundedI2)
   apply (erule order_trans [OF dist_triangle add_left_mono])
   done
 
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/NanoJava/OpSem.thy
--- a/src/HOL/NanoJava/OpSem.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/NanoJava/OpSem.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -86,15 +86,15 @@
 
 lemma exec_exec_max: "\<lbrakk>s1 -c1-    n1   \<rightarrow> t1 ; s2 -c2-       n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
                        s1 -c1-max n1 n2\<rightarrow> t1 \<and> s2 -c2-max n1 n2\<rightarrow> t2"
-by (fast intro: exec_mono le_maxI1 le_maxI2)
+by (fast intro: exec_mono max.cobounded1 max.cobounded2)
 
 lemma eval_exec_max: "\<lbrakk>s1 -c-    n1   \<rightarrow> t1 ; s2 -e\<succ>v-       n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
                        s1 -c-max n1 n2\<rightarrow> t1 \<and> s2 -e\<succ>v-max n1 n2\<rightarrow> t2"
-by (fast intro: eval_mono exec_mono le_maxI1 le_maxI2)
+by (fast intro: eval_mono exec_mono max.cobounded1 max.cobounded2)
 
 lemma eval_eval_max: "\<lbrakk>s1 -e1\<succ>v1-    n1   \<rightarrow> t1 ; s2 -e2\<succ>v2-       n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
                        s1 -e1\<succ>v1-max n1 n2\<rightarrow> t1 \<and> s2 -e2\<succ>v2-max n1 n2\<rightarrow> t2"
-by (fast intro: eval_mono le_maxI1 le_maxI2)
+by (fast intro: eval_mono max.cobounded1 max.cobounded2)
 
 lemma eval_eval_exec_max: 
  "\<lbrakk>s1 -e1\<succ>v1-n1\<rightarrow> t1; s2 -e2\<succ>v2-n2\<rightarrow> t2; s3 -c-n3\<rightarrow> t3\<rbrakk> \<Longrightarrow> 
@@ -102,7 +102,7 @@
    s2 -e2\<succ>v2-max (max n1 n2) n3\<rightarrow> t2 \<and> 
    s3 -c    -max (max n1 n2) n3\<rightarrow> t3"
 apply (drule (1) eval_eval_max, erule thin_rl)
-by (fast intro: exec_mono eval_mono le_maxI1 le_maxI2)
+by (fast intro: exec_mono eval_mono max.cobounded1 max.cobounded2)
 
 lemma Impl_body_eq: "(\<lambda>t. \<exists>n. Z -Impl M-n\<rightarrow> t) = (\<lambda>t. \<exists>n. Z -body M-n\<rightarrow> t)"
 apply (rule ext)
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Probability/Binary_Product_Measure.thy
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -324,7 +324,7 @@
         using `incseq F1` `incseq F2` unfolding incseq_def
         by (force split: split_max)+
       then have "(fst x, snd x) \<in> F1 (max i j) \<times> F2 (max i j)"
-        by (intro SigmaI) (auto simp add: min_max.sup_commute)
+        by (intro SigmaI) (auto simp add: max.commute)
       then show "x \<in> (\<Union>i. ?F i)" by auto
     qed
     then show "(\<Union>i. ?F i) = space M1 \<times> space M2"
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -795,7 +795,7 @@
 
     { fix z
       from F(4)[of z] have "F i z \<le> ereal (f z)"
-        by (metis SUP_upper UNIV_I ereal_max_0 min_max.sup_absorb2 nonneg)
+        by (metis SUP_upper UNIV_I ereal_max_0 max.absorb2 nonneg)
       with F(5)[of i z] have "real (F i z) \<le> f z"
         by (cases "F i z") simp_all }
     note F_bound = this
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Quotient_Examples/Quotient_Int.thy
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -187,7 +187,7 @@
 
 instance
   by default
-     (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
+     (auto simp add: inf_int_def sup_int_def max_min_distrib2)
 
 end
 
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Rat.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -494,7 +494,7 @@
   "(sup :: rat \<Rightarrow> rat \<Rightarrow> rat) = max"
 
 instance proof
-qed (auto simp add: inf_rat_def sup_rat_def min_max.sup_inf_distrib1)
+qed (auto simp add: inf_rat_def sup_rat_def max_min_distrib2)
 
 end
 
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Real.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -632,7 +632,7 @@
   "(sup :: real \<Rightarrow> real \<Rightarrow> real) = max"
 
 instance proof
-qed (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)
+qed (auto simp add: inf_real_def sup_real_def max_min_distrib2)
 
 end
 
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -1097,12 +1097,12 @@
   show ?thesis
   proof (intro exI impI conjI allI)
     show "0 < max 1 K"
-      by (rule order_less_le_trans [OF zero_less_one le_maxI1])
+      by (rule order_less_le_trans [OF zero_less_one max.cobounded1])
   next
     fix x
     have "norm (f x) \<le> norm x * K" using K .
     also have "\<dots> \<le> norm x * max 1 K"
-      by (rule mult_left_mono [OF le_maxI2 norm_ge_zero])
+      by (rule mult_left_mono [OF max.cobounded2 norm_ge_zero])
     finally show "norm (f x) \<le> norm x * max 1 K" .
   qed
 qed
@@ -1138,9 +1138,9 @@
   "\<exists>K>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K"
 apply (cut_tac bounded, erule exE)
 apply (rule_tac x="max 1 K" in exI, safe)
-apply (rule order_less_le_trans [OF zero_less_one le_maxI1])
+apply (rule order_less_le_trans [OF zero_less_one max.cobounded1])
 apply (drule spec, drule spec, erule order_trans)
-apply (rule mult_left_mono [OF le_maxI2])
+apply (rule mult_left_mono [OF max.cobounded2])
 apply (intro mult_nonneg_nonneg norm_ge_zero)
 done
 
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/UNITY/Simple/Common.thy
--- a/src/HOL/UNITY/Simple/Common.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/UNITY/Simple/Common.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -65,7 +65,7 @@
 lemma "mk_total_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)
        \<in> {m} co (maxfg m)"
 apply (simp add: mk_total_program_def) 
-apply (simp add: constrains_def maxfg_def gasc min_max.sup_absorb2)
+apply (simp add: constrains_def maxfg_def gasc max.absorb2)
 done
 
 (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
@@ -73,7 +73,7 @@
           (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)   
        \<in> {m} co (maxfg m)"
 apply (simp add: mk_total_program_def) 
-apply (simp add: constrains_def maxfg_def gasc min_max.sup_absorb2)
+apply (simp add: constrains_def maxfg_def gasc max.absorb2)
 done
 
 
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -420,7 +420,7 @@
 lemma sbintrunc_sbintrunc_min [simp]:
   "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
   apply (rule bin_eqI)
-  apply (auto simp: nth_sbintr min_max.inf_absorb1 min_max.inf_absorb2)
+  apply (auto simp: nth_sbintr min.absorb1 min.absorb2)
   done
 
 lemmas bintrunc_Pls = 
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -906,7 +906,7 @@
   apply (drule meta_spec)
   apply (erule trans)
   apply (drule_tac x = "bin_cat y n a" in meta_spec)
-  apply (simp add : bin_cat_assoc_sym min_max.inf_absorb2)
+  apply (simp add : bin_cat_assoc_sym min.absorb2)
   done
 
 lemma bin_rcat_bl:
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Word/Misc_Numeric.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -20,7 +20,7 @@
 
 lemma min_minus [simp] : "min m (m - k) = (m - k :: nat)" by arith
   
-lemmas min_minus' [simp] = trans [OF min_max.inf_commute min_minus]
+lemmas min_minus' [simp] = trans [OF min.commute min_minus]
 
 lemma mod_2_neq_1_eq_eq_0:
   fixes k :: int
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Word/Word.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -569,13 +569,13 @@
   shows "len_of TYPE('a) \<le> n \<Longrightarrow> bintrunc n (uint w) = uint w"
   apply (subst word_ubin.norm_Rep [symmetric]) 
   apply (simp only: bintrunc_bintrunc_min word_size)
-  apply (simp add: min_max.inf_absorb2)
+  apply (simp add: min.absorb2)
   done
 
 lemma wi_bintr:
   "len_of TYPE('a::len0) \<le> n \<Longrightarrow>
     word_of_int (bintrunc n w) = (word_of_int w :: 'a word)"
-  by (clarsimp simp add: word_ubin.norm_eq_iff [symmetric] min_max.inf_absorb1)
+  by (clarsimp simp add: word_ubin.norm_eq_iff [symmetric] min.absorb1)
 
 lemma td_ext_sbin: 
   "td_ext (sint :: 'a word => int) word_of_int (sints (len_of TYPE('a::len))) 
@@ -3692,7 +3692,7 @@
   word_of_int (bin_cat w (size b) (uint b))"
   apply (unfold word_cat_def word_size) 
   apply (clarsimp simp add: word_ubin.norm_eq_iff [symmetric]
-      word_ubin.eq_norm bintr_cat min_max.inf_absorb1)
+      word_ubin.eq_norm bintr_cat min.absorb1)
   done
 
 lemma word_cat_split_alt:
diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/ex/Dedekind_Real.thy
--- a/src/HOL/ex/Dedekind_Real.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/ex/Dedekind_Real.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -220,7 +220,7 @@
 
 instance
   by intro_classes
-    (auto simp add: inf_preal_def sup_preal_def min_max.sup_inf_distrib1)
+    (auto simp add: inf_preal_def sup_preal_def max_min_distrib2)
 
 end
 
@@ -1555,7 +1555,7 @@
   "(sup \<Colon> real \<Rightarrow> real \<Rightarrow> real) = max"
 
 instance
-  by default (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)
+  by default (auto simp add: inf_real_def sup_real_def max_min_distrib2)
 
 end