moved linorder_cases to theory Ord;

--- a/src/HOL/Typedef.thy	Wed Oct 03 20:53:02 2001 +0200
+++ b/src/HOL/Typedef.thy	Wed Oct 03 20:54:05 2001 +0200
@@ -9,11 +9,6 @@
 files "subset.ML" "equalities.ML" "mono.ML"
   "Tools/induct_attrib.ML" ("Tools/typedef_package.ML"):
 
-(** belongs to theory Ord **)
-  
-theorems linorder_cases [case_names less equal greater] =
-  linorder_less_split
-
 (* Courtesy of Stephan Merz *)
 lemma Least_mono: 
   "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y