src/HOL/Orderings.thy
changeset 22548 6ce4bddf3bcb
parent 22473 753123c89d72
child 22738 4899f06effc6
     1.1 --- a/src/HOL/Orderings.thy	Thu Mar 29 11:59:54 2007 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Thu Mar 29 14:21:45 2007 +0200
     1.3 @@ -901,26 +901,12 @@
     1.4      "(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)"
     1.5    by (simp add: max_def)
     1.6  
     1.7 -subsection {* Basic ML bindings *}
     1.8 +
     1.9 +subsection {* legacy ML bindings *}
    1.10  
    1.11  ML {*
    1.12 -val leD = thm "leD";
    1.13 -val leI = thm "leI";
    1.14 -val linorder_neqE = thm "linorder_neqE";
    1.15 -val linorder_neq_iff = thm "linorder_neq_iff";
    1.16 -val linorder_not_le = thm "linorder_not_le";
    1.17 -val linorder_not_less = thm "linorder_not_less";
    1.18 -val monoD = thm "monoD";
    1.19 -val monoI = thm "monoI";
    1.20 -val order_antisym = thm "order_antisym";
    1.21 -val order_less_irrefl = thm "order_less_irrefl";
    1.22 -val order_refl = thm "order_refl";
    1.23 -val order_trans = thm "order_trans";
    1.24 -val split_max = thm "split_max";
    1.25 -val split_min = thm "split_min";
    1.26 -*}
    1.27 +val monoI = @{thm monoI};
    1.28  
    1.29 -ML {*
    1.30  structure HOL =
    1.31  struct
    1.32    val thy = theory "HOL";