Orderings.min/max: no need to qualify consts;
authorwenzelm
Sat Nov 10 18:36:06 2007 +0100 (2007-11-10)
changeset 25377dcde128c84a2
parent 25376 87824cc5ff90
child 25378 dca691610489
Orderings.min/max: no need to qualify consts;
removed legacy ML bindings;
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/Orderings.thy	Sat Nov 10 15:58:18 2007 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Sat Nov 10 18:36:06 2007 +0100
     1.3 @@ -1055,12 +1055,12 @@
     1.4  
     1.5  lemma min_of_mono:
     1.6    fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
     1.7 -  shows "mono f \<Longrightarrow> Orderings.min (f m) (f n) = f (min m n)"
     1.8 +  shows "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)"
     1.9    by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
    1.10  
    1.11  lemma max_of_mono:
    1.12    fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
    1.13 -  shows "mono f \<Longrightarrow> Orderings.max (f m) (f n) = f (max m n)"
    1.14 +  shows "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)"
    1.15    by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym)
    1.16  
    1.17  end
    1.18 @@ -1108,10 +1108,4 @@
    1.19  apply (blast intro: order_antisym)
    1.20  done
    1.21  
    1.22 -subsection {* legacy ML bindings *}
    1.23 -
    1.24 -ML {*
    1.25 -val monoI = @{thm monoI};
    1.26 -*}
    1.27 -
    1.28  end