src/HOL/HOL.ML
author wenzelm
Sun Oct 28 21:14:56 2001 +0100 (2001-10-28)
changeset 11977 2e7c54b86763
parent 11749 fc8afdc58b26
child 12999 8ad8d02b973f
permissions -rw-r--r--
tuned declaration of rules;
wenzelm@10011
     1
(*  Title:      HOL/HOL.ML
wenzelm@10011
     2
    ID:         $Id$
wenzelm@10011
     3
*)
wenzelm@10011
     4
wenzelm@7357
     5
structure HOL =
wenzelm@7357
     6
struct
wenzelm@7357
     7
  val thy = the_context ();
wenzelm@7357
     8
  val plusI = plusI;
wenzelm@7357
     9
  val minusI = minusI;
wenzelm@7357
    10
  val timesI = timesI;
wenzelm@7357
    11
  val eq_reflection = eq_reflection;
wenzelm@7357
    12
  val refl = refl;
wenzelm@7357
    13
  val subst = subst;
wenzelm@7357
    14
  val ext = ext;
wenzelm@7357
    15
  val impI = impI;
wenzelm@7357
    16
  val mp = mp;
wenzelm@7357
    17
  val True_def = True_def;
wenzelm@7357
    18
  val All_def = All_def;
wenzelm@7357
    19
  val Ex_def = Ex_def;
wenzelm@7357
    20
  val False_def = False_def;
wenzelm@7357
    21
  val not_def = not_def;
wenzelm@7357
    22
  val and_def = and_def;
wenzelm@7357
    23
  val or_def = or_def;
wenzelm@7357
    24
  val Ex1_def = Ex1_def;
wenzelm@7357
    25
  val iff = iff;
wenzelm@7357
    26
  val True_or_False = True_or_False;
wenzelm@7357
    27
  val Let_def = Let_def;
wenzelm@7357
    28
  val if_def = if_def;
wenzelm@7357
    29
  val arbitrary_def = arbitrary_def;
wenzelm@3621
    30
end;
wenzelm@5888
    31
wenzelm@7357
    32
open HOL;
wenzelm@11749
    33
wenzelm@11749
    34
val Least_def = thm "Least_def";
wenzelm@11749
    35
val Least_equality = thm "Least_equality";
wenzelm@11749
    36
val mono_def = thm "mono_def";
wenzelm@11749
    37
val monoI = thm "monoI";
wenzelm@11749
    38
val monoD = thm "monoD";
wenzelm@11749
    39
val min_def = thm "min_def";
wenzelm@11749
    40
val min_of_mono = thm "min_of_mono";
wenzelm@11749
    41
val max_def = thm "max_def";
wenzelm@11749
    42
val max_of_mono = thm "max_of_mono";
wenzelm@11749
    43
val min_leastL = thm "min_leastL";
wenzelm@11749
    44
val max_leastL = thm "max_leastL";
wenzelm@11749
    45
val min_leastR = thm "min_leastR";
wenzelm@11749
    46
val max_leastR = thm "max_leastR";
wenzelm@11749
    47
val order_eq_refl = thm "order_eq_refl";
wenzelm@11749
    48
val order_less_irrefl = thm "order_less_irrefl";
wenzelm@11749
    49
val order_le_less = thm "order_le_less";
wenzelm@11749
    50
val order_le_imp_less_or_eq = thm "order_le_imp_less_or_eq";
wenzelm@11749
    51
val order_less_imp_le = thm "order_less_imp_le";
wenzelm@11749
    52
val order_less_not_sym = thm "order_less_not_sym";
wenzelm@11749
    53
val order_less_asym = thm "order_less_asym";
wenzelm@11749
    54
val order_less_trans = thm "order_less_trans";
wenzelm@11749
    55
val order_le_less_trans = thm "order_le_less_trans";
wenzelm@11749
    56
val order_less_le_trans = thm "order_less_le_trans";
wenzelm@11749
    57
val order_less_imp_not_less = thm "order_less_imp_not_less";
wenzelm@11749
    58
val order_less_imp_triv = thm "order_less_imp_triv";
wenzelm@11749
    59
val order_less_imp_not_eq = thm "order_less_imp_not_eq";
wenzelm@11749
    60
val order_less_imp_not_eq2 = thm "order_less_imp_not_eq2";
wenzelm@11749
    61
val linorder_less_linear = thm "linorder_less_linear";
wenzelm@11749
    62
val linorder_cases = thm "linorder_cases";
wenzelm@11749
    63
val linorder_not_less = thm "linorder_not_less";
wenzelm@11749
    64
val linorder_not_le = thm "linorder_not_le";
wenzelm@11749
    65
val linorder_neq_iff = thm "linorder_neq_iff";
wenzelm@11749
    66
val linorder_neqE = thm "linorder_neqE";
wenzelm@11749
    67
val min_same = thm "min_same";
wenzelm@11749
    68
val max_same = thm "max_same";
wenzelm@11749
    69
val le_max_iff_disj = thm "le_max_iff_disj";
wenzelm@11749
    70
val le_maxI1 = thm "le_maxI1";
wenzelm@11749
    71
val le_maxI2 = thm "le_maxI2";
wenzelm@11749
    72
val less_max_iff_disj = thm "less_max_iff_disj";
wenzelm@11749
    73
val max_le_iff_conj = thm "max_le_iff_conj";
wenzelm@11749
    74
val max_less_iff_conj = thm "max_less_iff_conj";
wenzelm@11749
    75
val le_min_iff_conj = thm "le_min_iff_conj";
wenzelm@11749
    76
val min_less_iff_conj = thm "min_less_iff_conj";
wenzelm@11749
    77
val min_le_iff_disj = thm "min_le_iff_disj";
wenzelm@11749
    78
val min_less_iff_disj = thm "min_less_iff_disj";
wenzelm@11749
    79
val split_min = thm "split_min";
wenzelm@11749
    80
val split_max = thm "split_max";
wenzelm@11749
    81
val order_refl = thm "order_refl";
wenzelm@11749
    82
val order_trans = thm "order_trans";
wenzelm@11749
    83
val order_antisym = thm "order_antisym";
wenzelm@11749
    84
val order_less_le = thm "order_less_le";
wenzelm@11749
    85
val linorder_linear = thm "linorder_linear";