src/HOL/Orderings.ML
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 21216 1c8580913738
child 21619 dea0914773f7
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
nipkow@15524
     1
(* legacy ML bindings *)
nipkow@15524
     2
nipkow@15524
     3
val order_eq_refl = thm "order_eq_refl";
nipkow@15524
     4
val order_less_irrefl = thm "order_less_irrefl";
nipkow@15524
     5
val order_le_less = thm "order_le_less";
nipkow@15524
     6
val order_le_imp_less_or_eq = thm "order_le_imp_less_or_eq";
nipkow@15524
     7
val order_less_imp_le = thm "order_less_imp_le";
nipkow@15524
     8
val order_less_not_sym = thm "order_less_not_sym";
nipkow@15524
     9
val order_less_asym = thm "order_less_asym";
nipkow@15524
    10
val order_less_trans = thm "order_less_trans";
nipkow@15524
    11
val order_le_less_trans = thm "order_le_less_trans";
nipkow@15524
    12
val order_less_le_trans = thm "order_less_le_trans";
nipkow@15524
    13
val order_less_imp_not_less = thm "order_less_imp_not_less";
nipkow@15524
    14
val order_less_imp_triv = thm "order_less_imp_triv";
nipkow@15524
    15
val order_less_imp_not_eq = thm "order_less_imp_not_eq";
nipkow@15524
    16
val order_less_imp_not_eq2 = thm "order_less_imp_not_eq2";
nipkow@15524
    17
val linorder_less_linear = thm "linorder_less_linear";
nipkow@15524
    18
val linorder_cases = thm "linorder_cases";
nipkow@15524
    19
val linorder_not_less = thm "linorder_not_less";
nipkow@15524
    20
val linorder_not_le = thm "linorder_not_le";
nipkow@15524
    21
val linorder_neq_iff = thm "linorder_neq_iff";
nipkow@15524
    22
val linorder_neqE = thm "linorder_neqE";
nipkow@15524
    23
val order_refl = thm "order_refl";
nipkow@15524
    24
val order_trans = thm "order_trans";
nipkow@15524
    25
val order_antisym = thm "order_antisym";
nipkow@15524
    26
val order_less_le = thm "order_less_le";
nipkow@15524
    27
val linorder_linear = thm "linorder_linear";
haftmann@21216
    28
val mono_def = thm "mono_def";
haftmann@21216
    29
val monoI = thm "monoI";
haftmann@21216
    30
val monoD = thm "monoD";