--- a/src/HOL/HOL.thy Wed Jul 24 00:09:44 2002 +0200
+++ b/src/HOL/HOL.thy Wed Jul 24 00:10:52 2002 +0200
@@ -601,15 +601,17 @@
subsubsection {* Monotonicity *}
-constdefs
- mono :: "['a::ord => 'b::ord] => bool"
- "mono f == ALL A B. A <= B --> f A <= f B"
+locale mono =
+ fixes f
+ assumes mono: "A <= B ==> f A <= f B"
-lemma monoI [intro?]: "(!!A B. A <= B ==> f A <= f B) ==> mono f"
- by (unfold mono_def) rules
+lemmas monoI [intro?] = mono.intro [OF mono_axioms.intro]
+ and monoD [dest?] = mono.mono
-lemma monoD [dest?]: "mono f ==> A <= B ==> f A <= f B"
- by (unfold mono_def) rules
+lemma mono_def: "mono f == ALL A B. A <= B --> f A <= f B"
+ -- compatibility
+ by (simp only: atomize_eq mono_def mono_axioms_def)
+
constdefs
min :: "['a::ord, 'a] => 'a"