src/HOL/HOL.ML
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 21379 a0561695167a
child 21546 268b6bed0cc8
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
wenzelm@12999
     1
(* legacy ML bindings *)
wenzelm@11749
     2
haftmann@20973
     3
val HOL_cs = HOL.claset;
haftmann@20973
     4
val HOL_basic_ss = HOL.simpset_basic;
haftmann@20973
     5
val HOL_ss = HOL.simpset;
haftmann@20973
     6
val hol_simplify = HOL.simplify;
haftmann@20973
     7
haftmann@20973
     8
val split_tac        = Splitter.split_tac;
haftmann@20973
     9
val split_inside_tac = Splitter.split_inside_tac;
haftmann@20973
    10
val split_asm_tac    = Splitter.split_asm_tac;
haftmann@20973
    11
val op addsplits     = Splitter.addsplits;
haftmann@20973
    12
val op delsplits     = Splitter.delsplits;
haftmann@20973
    13
val Addsplits        = Splitter.Addsplits;
haftmann@20973
    14
val Delsplits        = Splitter.Delsplits;
haftmann@20973
    15
haftmann@20944
    16
open HOL;
haftmann@20973
    17
val claset = Classical.claset;
haftmann@20973
    18
val simpset = Simplifier.simpset;
haftmann@20973
    19
val simplify = Simplifier.simplify;
haftmann@21009
    20
open Hypsubst;
haftmann@21009
    21
open BasicClassical;
haftmann@20973
    22
open Clasimp;
wenzelm@12999
    23
haftmann@20944
    24
val ext = thm "ext"
haftmann@20944
    25
val True_def = thm "True_def"
haftmann@20944
    26
val All_def = thm "All_def"
haftmann@20944
    27
val Ex_def = thm "Ex_def"
haftmann@20944
    28
val False_def = thm "False_def"
haftmann@20944
    29
val not_def = thm "not_def"
haftmann@20944
    30
val and_def = thm "and_def"
haftmann@20944
    31
val or_def = thm "or_def"
haftmann@20944
    32
val Ex1_def = thm "Ex1_def"
haftmann@20944
    33
val iff = thm "iff"
haftmann@20944
    34
val True_or_False = thm "True_or_False"
haftmann@20944
    35
val Let_def = thm "Let_def"
haftmann@20944
    36
val if_def = thm "if_def"
haftmann@20944
    37
val ssubst = thm "ssubst"
haftmann@20944
    38
val box_equals = thm "box_equals"
haftmann@20944
    39
val fun_cong = thm "fun_cong"
haftmann@20944
    40
val cong = thm "cong"
haftmann@20944
    41
val rev_iffD2 = thm "rev_iffD2"
haftmann@20944
    42
val rev_iffD1 = thm "rev_iffD1"
haftmann@20944
    43
val iffE = thm "iffE"
haftmann@20944
    44
val eqTrueI = thm "eqTrueI"
haftmann@20944
    45
val eqTrueE = thm "eqTrueE"
haftmann@20944
    46
val all_dupE = thm "all_dupE"
haftmann@20944
    47
val FalseE = thm "FalseE"
haftmann@20944
    48
val False_neq_True = thm "False_neq_True"
haftmann@20944
    49
val False_not_True = thm "False_not_True"
haftmann@20944
    50
val True_not_False = thm "True_not_False"
haftmann@20944
    51
val notI2 = thm "notI2"
haftmann@20944
    52
val impE = thm "impE"
haftmann@20944
    53
val not_sym = thm "not_sym"
haftmann@20944
    54
val rev_contrapos = thm "rev_contrapos"
haftmann@20944
    55
val conjE = thm "conjE"
haftmann@20944
    56
val context_conjI = thm "context_conjI"
haftmann@20944
    57
val disjI1 = thm "disjI1"
haftmann@20944
    58
val disjI2 = thm "disjI2"
haftmann@20944
    59
val rev_notE = thm "rev_notE"
haftmann@20944
    60
val ex1I = thm "ex1I"
haftmann@20944
    61
val ex1E = thm "ex1E"
haftmann@20944
    62
val ex1_implies_ex = thm "ex1_implies_ex"
haftmann@20944
    63
val the_equality = thm "the_equality"
haftmann@20944
    64
val theI = thm "theI"
haftmann@20944
    65
val theI' = thm "theI'"
haftmann@20944
    66
val theI2 = thm "theI2"
haftmann@20944
    67
val the1_equality = thm "the1_equality"
haftmann@20944
    68
val excluded_middle = thm "excluded_middle"
haftmann@20944
    69
val case_split_thm = thm "case_split_thm"
haftmann@20944
    70
val exCI = thm "exCI"
haftmann@20944
    71
val choice_eq = thm "choice_eq"
haftmann@20944
    72
val eq_cong2 = thm "eq_cong2"
haftmann@20944
    73
val if_cong = thm "if_cong"
haftmann@20944
    74
val if_weak_cong = thm "if_weak_cong"
haftmann@20944
    75
val let_weak_cong = thm "let_weak_cong"
haftmann@20944
    76
val eq_cong2 = thm "eq_cong2"
haftmann@20944
    77
val if_distrib = thm "if_distrib"
haftmann@20944
    78
val expand_case = thm "expand_case"
haftmann@20944
    79
val restrict_to_left = thm "restrict_to_left"
haftmann@20944
    80
val all_conj_distrib = thm "all_conj_distrib";
haftmann@20944
    81
val atomize_not = thm "atomize_not";
haftmann@20944
    82
val split_if = thm "split_if";
haftmann@20944
    83
val split_if_asm = thm "split_if_asm";
haftmann@20944
    84
val rev_conj_cong = thm "rev_conj_cong";
haftmann@20944
    85
val not_all = thm "not_all";
haftmann@20944
    86
val not_ex = thm "not_ex";
haftmann@20944
    87
val not_iff = thm "not_iff";
haftmann@20944
    88
val not_imp = thm "not_imp";
haftmann@20944
    89
val not_not = thm "not_not";
haftmann@20944
    90
val eta_contract_eq = thm "eta_contract_eq";
haftmann@20944
    91
val eq_ac = thms "eq_ac";
haftmann@20944
    92
val eq_commute = thm "eq_commute";
haftmann@20944
    93
val eq_sym_conv = thm "eq_commute";
haftmann@20944
    94
val neq_commute = thm "neq_commute";
haftmann@20944
    95
val conj_comms = thms "conj_comms";
haftmann@20944
    96
val conj_commute = thm "conj_commute";
haftmann@20944
    97
val conj_cong = thm "conj_cong";
haftmann@20944
    98
val conj_disj_distribL = thm "conj_disj_distribL";
haftmann@20944
    99
val conj_disj_distribR = thm "conj_disj_distribR";
haftmann@20944
   100
val conj_left_commute = thm "conj_left_commute";
haftmann@20944
   101
val disj_comms = thms "disj_comms";
haftmann@20944
   102
val disj_commute = thm "disj_commute";
haftmann@20944
   103
val disj_cong = thm "disj_cong";
haftmann@20944
   104
val disj_conj_distribL = thm "disj_conj_distribL";
haftmann@20944
   105
val disj_conj_distribR = thm "disj_conj_distribR";
haftmann@20944
   106
val disj_left_commute = thm "disj_left_commute";
haftmann@20944
   107
val eq_assoc = thm "eq_assoc";
haftmann@20944
   108
val eq_left_commute = thm "eq_left_commute";
haftmann@20944
   109
val ex_disj_distrib = thm "ex_disj_distrib";
haftmann@20944
   110
val if_P = thm "if_P";
haftmann@20944
   111
val if_bool_eq_disj = thm "if_bool_eq_disj";
haftmann@20944
   112
val if_def2 = thm "if_bool_eq_conj";
haftmann@20944
   113
val if_not_P = thm "if_not_P";
haftmann@20944
   114
val if_splits = thms "if_splits";
haftmann@20944
   115
val imp_all = thm "imp_all";
haftmann@20944
   116
val imp_conjL = thm "imp_conjL";
haftmann@20944
   117
val imp_conjR = thm "imp_conjR";
haftmann@20944
   118
val imp_disj_not1 = thm "imp_disj_not1";
haftmann@20944
   119
val imp_disj_not2 = thm "imp_disj_not2";
haftmann@20944
   120
val imp_ex = thm "imp_ex";
haftmann@20944
   121
val meta_eq_to_obj_eq = thm "def_imp_eq";
haftmann@20944
   122
val ex_simps = thms "ex_simps";
haftmann@20944
   123
val all_simps = thms "all_simps";
haftmann@20944
   124
val simp_thms = thms "simp_thms";
haftmann@20944
   125
val Eq_FalseI = thm "Eq_FalseI";
haftmann@20944
   126
val Eq_TrueI = thm "Eq_TrueI";
haftmann@20944
   127
val cases_simp = thm "cases_simp";
haftmann@20944
   128
val conj_assoc = thm "conj_assoc";
haftmann@20944
   129
val de_Morgan_conj = thm "de_Morgan_conj";
haftmann@20944
   130
val de_Morgan_disj = thm "de_Morgan_disj";
haftmann@20944
   131
val disj_assoc = thm "disj_assoc";
haftmann@20944
   132
val disj_not1 = thm "disj_not1";
haftmann@20944
   133
val disj_not2 = thm "disj_not2";
haftmann@20944
   134
val if_False = thm "if_False";
haftmann@20944
   135
val if_True = thm "if_True";
haftmann@20944
   136
val if_bool_eq_conj = thm "if_bool_eq_conj";
haftmann@20944
   137
val if_cancel = thm "if_cancel";
haftmann@20944
   138
val if_eq_cancel = thm "if_eq_cancel";
haftmann@20944
   139
val iff_conv_conj_imp = thm "iff_conv_conj_imp";
haftmann@20944
   140
val imp_cong = thm "imp_cong";
haftmann@20944
   141
val imp_conv_disj = thm "imp_conv_disj";
haftmann@20944
   142
val imp_disj1 = thm "imp_disj1";
haftmann@20944
   143
val imp_disj2 = thm "imp_disj2";
haftmann@20944
   144
val imp_disjL = thm "imp_disjL";
haftmann@20944
   145
val simp_impliesI = thm "simp_impliesI";
haftmann@20944
   146
val simp_implies_cong = thm "simp_implies_cong";
haftmann@20944
   147
val simp_implies_def = thm "simp_implies_def";
haftmann@20944
   148
val True_implies_equals = thm "True_implies_equals";
haftmann@18916
   149
haftmann@18916
   150
structure HOL =
haftmann@18916
   151
struct
haftmann@18916
   152
haftmann@18916
   153
open HOL;
haftmann@18916
   154
haftmann@18916
   155
val thy = the_context ();
haftmann@18916
   156
haftmann@18916
   157
end;