src/HOL/Typedef.thy
changeset 11654 53d18ab990f6
parent 11608 c760ea8154ee
child 11659 a68f930bafb2
     1.1 --- a/src/HOL/Typedef.thy	Wed Oct 03 20:53:02 2001 +0200
     1.2 +++ b/src/HOL/Typedef.thy	Wed Oct 03 20:54:05 2001 +0200
     1.3 @@ -9,11 +9,6 @@
     1.4  files "subset.ML" "equalities.ML" "mono.ML"
     1.5    "Tools/induct_attrib.ML" ("Tools/typedef_package.ML"):
     1.6  
     1.7 -(** belongs to theory Ord **)
     1.8 -  
     1.9 -theorems linorder_cases [case_names less equal greater] =
    1.10 -  linorder_less_split
    1.11 -
    1.12  (* Courtesy of Stephan Merz *)
    1.13  lemma Least_mono: 
    1.14    "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y