--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Ord.ML	Thu Sep 16 12:21:07 1993 +0200
@@ -0,0 +1,13 @@
+open Ord;
+
+val [prem] = goalw Ord.thy [mono_def]
+    "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
+by (REPEAT (ares_tac [allI, impI, prem] 1));
+val monoI = result();
+
+val [major,minor] = goalw Ord.thy [mono_def]
+    "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
+by (rtac (major RS spec RS spec RS mp) 1);
+by (rtac minor 1);
+val monoD = result();
+