src/HOL/Orderings.ML
author haftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 20380 14f9f2a1caa6
parent 15791 446ec11266be
child 21216 1c8580913738
permissions -rw-r--r--
simplified code generator setup
nipkow@15524
     1
(* legacy ML bindings *)
nipkow@15524
     2
nipkow@15524
     3
val Least_def = thm "Least_def";
nipkow@15524
     4
val Least_equality = thm "Least_equality";
nipkow@15524
     5
val mono_def = thm "mono_def";
nipkow@15524
     6
val monoI = thm "monoI";
nipkow@15524
     7
val monoD = thm "monoD";
nipkow@15524
     8
val min_def = thm "min_def";
nipkow@15524
     9
val min_of_mono = thm "min_of_mono";
nipkow@15524
    10
val max_def = thm "max_def";
nipkow@15524
    11
val max_of_mono = thm "max_of_mono";
nipkow@15524
    12
val min_leastL = thm "min_leastL";
nipkow@15524
    13
val max_leastL = thm "max_leastL";
nipkow@15524
    14
val min_leastR = thm "min_leastR";
nipkow@15524
    15
val max_leastR = thm "max_leastR";
nipkow@15524
    16
val order_eq_refl = thm "order_eq_refl";
nipkow@15524
    17
val order_less_irrefl = thm "order_less_irrefl";
nipkow@15524
    18
val order_le_less = thm "order_le_less";
nipkow@15524
    19
val order_le_imp_less_or_eq = thm "order_le_imp_less_or_eq";
nipkow@15524
    20
val order_less_imp_le = thm "order_less_imp_le";
nipkow@15524
    21
val order_less_not_sym = thm "order_less_not_sym";
nipkow@15524
    22
val order_less_asym = thm "order_less_asym";
nipkow@15524
    23
val order_less_trans = thm "order_less_trans";
nipkow@15524
    24
val order_le_less_trans = thm "order_le_less_trans";
nipkow@15524
    25
val order_less_le_trans = thm "order_less_le_trans";
nipkow@15524
    26
val order_less_imp_not_less = thm "order_less_imp_not_less";
nipkow@15524
    27
val order_less_imp_triv = thm "order_less_imp_triv";
nipkow@15524
    28
val order_less_imp_not_eq = thm "order_less_imp_not_eq";
nipkow@15524
    29
val order_less_imp_not_eq2 = thm "order_less_imp_not_eq2";
nipkow@15524
    30
val linorder_less_linear = thm "linorder_less_linear";
nipkow@15524
    31
val linorder_cases = thm "linorder_cases";
nipkow@15524
    32
val linorder_not_less = thm "linorder_not_less";
nipkow@15524
    33
val linorder_not_le = thm "linorder_not_le";
nipkow@15524
    34
val linorder_neq_iff = thm "linorder_neq_iff";
nipkow@15524
    35
val linorder_neqE = thm "linorder_neqE";
nipkow@15791
    36
(*
nipkow@15524
    37
val min_same = thm "min_same";
nipkow@15524
    38
val max_same = thm "max_same";
nipkow@15791
    39
*)
nipkow@15524
    40
val le_max_iff_disj = thm "le_max_iff_disj";
nipkow@15524
    41
val le_maxI1 = thm "le_maxI1";
nipkow@15524
    42
val le_maxI2 = thm "le_maxI2";
nipkow@15524
    43
val less_max_iff_disj = thm "less_max_iff_disj";
nipkow@15524
    44
val max_less_iff_conj = thm "max_less_iff_conj";
nipkow@15524
    45
val min_less_iff_conj = thm "min_less_iff_conj";
nipkow@15524
    46
val min_le_iff_disj = thm "min_le_iff_disj";
nipkow@15524
    47
val min_less_iff_disj = thm "min_less_iff_disj";
nipkow@15524
    48
val split_min = thm "split_min";
nipkow@15524
    49
val split_max = thm "split_max";
nipkow@15524
    50
val order_refl = thm "order_refl";
nipkow@15524
    51
val order_trans = thm "order_trans";
nipkow@15524
    52
val order_antisym = thm "order_antisym";
nipkow@15524
    53
val order_less_le = thm "order_less_le";
nipkow@15524
    54
val linorder_linear = thm "linorder_linear";