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