diff -r f04b33ce250f -r a4dc62a46ee4 Ord.ML
--- a/Ord.ML	Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-(*  Title: 	HOL/Ord.ML
-    ID:         $Id$
-    Author: 	Tobias Nipkow, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-The type class for ordered types
-*)
-
-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));
-qed "monoI";
-
-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);
-qed "monoD";
-