diff -r bab2371e0348 -r 2ff24d87fad1 src/HOL/AxClasses/Lattice/OrdInsts.thy
--- a/src/HOL/AxClasses/Lattice/OrdInsts.thy	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(*  Title:      OrdInsts.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Some order instantiations.
-*)
-
-OrdInsts = OrdDefs +
-
-
-(* binary / general products of quasi_orders / orders *)
-
-instance
-  "*" :: (quasi_order, quasi_order) quasi_order         (le_prod_refl, le_prod_trans)
-
-instance
-  "*" :: (partial_order, partial_order) partial_order   (le_prod_antisym)
-  
-
-instance
-  fun :: (term, quasi_order) quasi_order                (le_fun_refl, le_fun_trans)
-
-instance
-  fun :: (term, partial_order) partial_order            (le_fun_antisym)
-
-
-(* duals of quasi orders / partial orders / linear orders *)
-
-instance
-  dual :: (quasi_order) quasi_order                     (le_dual_refl, le_dual_trans)
-
-instance
-  dual :: (partial_order) partial_order                 (le_dual_antisym)
-
-
-(*FIXME: had to be moved to LatInsts.thy due to some unpleasant
-  'feature' in Pure/type.ML
-
-instance
-  dual :: (linear_order) linear_order                   (le_dual_lin)
-*)
-
-end