--- 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