# HG changeset patch
# User wenzelm
# Date 1002135245 -7200
# Node ID 53d18ab990f65c3e6c1e8ecfa900802a7285b263
# Parent  93aaafb6431b638668fcb9cf2076831f535daad4
moved linorder_cases to theory Ord;

diff -r 93aaafb6431b -r 53d18ab990f6 src/HOL/Typedef.thy
--- 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