src/HOL/HOL.ML
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 14223 0ee05eef881b
child 15524 2ef571f80a55
permissions -rw-r--r--
import -> imports
     1 
     2 (* legacy ML bindings *)
     3 
     4 val Least_def = thm "Least_def";
     5 val Least_equality = thm "Least_equality";
     6 val mono_def = thm "mono_def";
     7 val monoI = thm "monoI";
     8 val monoD = thm "monoD";
     9 val min_def = thm "min_def";
    10 val min_of_mono = thm "min_of_mono";
    11 val max_def = thm "max_def";
    12 val max_of_mono = thm "max_of_mono";
    13 val min_leastL = thm "min_leastL";
    14 val max_leastL = thm "max_leastL";
    15 val min_leastR = thm "min_leastR";
    16 val max_leastR = thm "max_leastR";
    17 val order_eq_refl = thm "order_eq_refl";
    18 val order_less_irrefl = thm "order_less_irrefl";
    19 val order_le_less = thm "order_le_less";
    20 val order_le_imp_less_or_eq = thm "order_le_imp_less_or_eq";
    21 val order_less_imp_le = thm "order_less_imp_le";
    22 val order_less_not_sym = thm "order_less_not_sym";
    23 val order_less_asym = thm "order_less_asym";
    24 val order_less_trans = thm "order_less_trans";
    25 val order_le_less_trans = thm "order_le_less_trans";
    26 val order_less_le_trans = thm "order_less_le_trans";
    27 val order_less_imp_not_less = thm "order_less_imp_not_less";
    28 val order_less_imp_triv = thm "order_less_imp_triv";
    29 val order_less_imp_not_eq = thm "order_less_imp_not_eq";
    30 val order_less_imp_not_eq2 = thm "order_less_imp_not_eq2";
    31 val linorder_less_linear = thm "linorder_less_linear";
    32 val linorder_cases = thm "linorder_cases";
    33 val linorder_not_less = thm "linorder_not_less";
    34 val linorder_not_le = thm "linorder_not_le";
    35 val linorder_neq_iff = thm "linorder_neq_iff";
    36 val linorder_neqE = thm "linorder_neqE";
    37 val min_same = thm "min_same";
    38 val max_same = thm "max_same";
    39 val le_max_iff_disj = thm "le_max_iff_disj";
    40 val le_maxI1 = thm "le_maxI1";
    41 val le_maxI2 = thm "le_maxI2";
    42 val less_max_iff_disj = thm "less_max_iff_disj";
    43 val max_le_iff_conj = thm "max_le_iff_conj";
    44 val max_less_iff_conj = thm "max_less_iff_conj";
    45 val le_min_iff_conj = thm "le_min_iff_conj";
    46 val min_less_iff_conj = thm "min_less_iff_conj";
    47 val min_le_iff_disj = thm "min_le_iff_disj";
    48 val min_less_iff_disj = thm "min_less_iff_disj";
    49 val split_min = thm "split_min";
    50 val split_max = thm "split_max";
    51 val order_refl = thm "order_refl";
    52 val order_trans = thm "order_trans";
    53 val order_antisym = thm "order_antisym";
    54 val order_less_le = thm "order_less_le";
    55 val linorder_linear = thm "linorder_linear";
    56 val choice_eq = thm "choice_eq";
    57 
    58 structure HOL =
    59 struct
    60   val thy = the_context ();
    61   val plusI = plusI;
    62   val minusI = minusI;
    63   val timesI = timesI;
    64   val eq_reflection = eq_reflection;
    65   val refl = refl;
    66   val subst = subst;
    67   val ext = ext;
    68   val impI = impI;
    69   val mp = mp;
    70   val True_def = True_def;
    71   val All_def = All_def;
    72   val Ex_def = Ex_def;
    73   val False_def = False_def;
    74   val not_def = not_def;
    75   val and_def = and_def;
    76   val or_def = or_def;
    77   val Ex1_def = Ex1_def;
    78   val iff = iff;
    79   val True_or_False = True_or_False;
    80   val Let_def = Let_def;
    81   val if_def = if_def;
    82 end;
    83 
    84 open HOL;