# HG changeset patch
# User wenzelm
# Date 1194716166 -3600
# Node ID dcde128c84a2156fe8c19e4fe523d2548305413d
# Parent  87824cc5ff90835eb3f04bbcda72ea900b30d8a8
Orderings.min/max: no need to qualify consts;
removed legacy ML bindings;

diff -r 87824cc5ff90 -r dcde128c84a2 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sat Nov 10 15:58:18 2007 +0100
+++ b/src/HOL/Orderings.thy	Sat Nov 10 18:36:06 2007 +0100
@@ -1055,12 +1055,12 @@
 
 lemma min_of_mono:
   fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
-  shows "mono f \<Longrightarrow> Orderings.min (f m) (f n) = f (min m n)"
+  shows "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)"
   by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
 
 lemma max_of_mono:
   fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
-  shows "mono f \<Longrightarrow> Orderings.max (f m) (f n) = f (max m n)"
+  shows "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)"
   by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym)
 
 end
@@ -1108,10 +1108,4 @@
 apply (blast intro: order_antisym)
 done
 
-subsection {* legacy ML bindings *}
-
-ML {*
-val monoI = @{thm monoI};
-*}
-
 end