added ML bindings from former theory Ord;
authorwenzelm
Sun Oct 14 20:00:32 2001 +0200 (2001-10-14)
changeset 11749fc8afdc58b26
parent 11748 06eb315831ff
child 11750 3e400964893e
added ML bindings from former theory Ord;
src/HOL/HOL.ML
     1.1 --- a/src/HOL/HOL.ML	Sun Oct 14 19:59:55 2001 +0200
     1.2 +++ b/src/HOL/HOL.ML	Sun Oct 14 20:00:32 2001 +0200
     1.3 @@ -33,3 +33,56 @@
     1.4  AddXEs [disjI1, disjI2, ex1_implies_ex, sym];
     1.5  
     1.6  open HOL;
     1.7 +
     1.8 +val Least_def = thm "Least_def";
     1.9 +val Least_equality = thm "Least_equality";
    1.10 +val mono_def = thm "mono_def";
    1.11 +val monoI = thm "monoI";
    1.12 +val monoD = thm "monoD";
    1.13 +val min_def = thm "min_def";
    1.14 +val min_of_mono = thm "min_of_mono";
    1.15 +val max_def = thm "max_def";
    1.16 +val max_of_mono = thm "max_of_mono";
    1.17 +val min_leastL = thm "min_leastL";
    1.18 +val max_leastL = thm "max_leastL";
    1.19 +val min_leastR = thm "min_leastR";
    1.20 +val max_leastR = thm "max_leastR";
    1.21 +val order_eq_refl = thm "order_eq_refl";
    1.22 +val order_less_irrefl = thm "order_less_irrefl";
    1.23 +val order_le_less = thm "order_le_less";
    1.24 +val order_le_imp_less_or_eq = thm "order_le_imp_less_or_eq";
    1.25 +val order_less_imp_le = thm "order_less_imp_le";
    1.26 +val order_less_not_sym = thm "order_less_not_sym";
    1.27 +val order_less_asym = thm "order_less_asym";
    1.28 +val order_less_trans = thm "order_less_trans";
    1.29 +val order_le_less_trans = thm "order_le_less_trans";
    1.30 +val order_less_le_trans = thm "order_less_le_trans";
    1.31 +val order_less_imp_not_less = thm "order_less_imp_not_less";
    1.32 +val order_less_imp_triv = thm "order_less_imp_triv";
    1.33 +val order_less_imp_not_eq = thm "order_less_imp_not_eq";
    1.34 +val order_less_imp_not_eq2 = thm "order_less_imp_not_eq2";
    1.35 +val linorder_less_linear = thm "linorder_less_linear";
    1.36 +val linorder_cases = thm "linorder_cases";
    1.37 +val linorder_not_less = thm "linorder_not_less";
    1.38 +val linorder_not_le = thm "linorder_not_le";
    1.39 +val linorder_neq_iff = thm "linorder_neq_iff";
    1.40 +val linorder_neqE = thm "linorder_neqE";
    1.41 +val min_same = thm "min_same";
    1.42 +val max_same = thm "max_same";
    1.43 +val le_max_iff_disj = thm "le_max_iff_disj";
    1.44 +val le_maxI1 = thm "le_maxI1";
    1.45 +val le_maxI2 = thm "le_maxI2";
    1.46 +val less_max_iff_disj = thm "less_max_iff_disj";
    1.47 +val max_le_iff_conj = thm "max_le_iff_conj";
    1.48 +val max_less_iff_conj = thm "max_less_iff_conj";
    1.49 +val le_min_iff_conj = thm "le_min_iff_conj";
    1.50 +val min_less_iff_conj = thm "min_less_iff_conj";
    1.51 +val min_le_iff_disj = thm "min_le_iff_disj";
    1.52 +val min_less_iff_disj = thm "min_less_iff_disj";
    1.53 +val split_min = thm "split_min";
    1.54 +val split_max = thm "split_max";
    1.55 +val order_refl = thm "order_refl";
    1.56 +val order_trans = thm "order_trans";
    1.57 +val order_antisym = thm "order_antisym";
    1.58 +val order_less_le = thm "order_less_le";
    1.59 +val linorder_linear = thm "linorder_linear";