src/HOL/HOL.ML
author haftmann
Fri Apr 20 11:21:42 2007 +0200 (2007-04-20)
changeset 22744 5cbe966d67a2
parent 22218 30a8890d2967
permissions -rw-r--r--
Isar definitions are now added explicitly to code theorem table
     1 (*
     2     ID:         $Id$
     3 *)
     4 
     5 (** legacy ML bindings **)
     6 
     7 val all_conj_distrib = thm "all_conj_distrib";
     8 val all_simps = thms "all_simps";
     9 val atomize_not = thm "atomize_not";
    10 val case_split = thm "case_split_thm";
    11 val case_split_thm = thm "case_split_thm"
    12 val cases_simp = thm "cases_simp";
    13 val choice_eq = thm "choice_eq"
    14 val cong = thm "cong"
    15 val conj_comms = thms "conj_comms";
    16 val conj_cong = thm "conj_cong";
    17 val de_Morgan_conj = thm "de_Morgan_conj";
    18 val de_Morgan_disj = thm "de_Morgan_disj";
    19 val disj_assoc = thm "disj_assoc";
    20 val disj_comms = thms "disj_comms";
    21 val disj_cong = thm "disj_cong";
    22 val eq_ac = thms "eq_ac";
    23 val eq_cong2 = thm "eq_cong2"
    24 val Eq_FalseI = thm "Eq_FalseI";
    25 val Eq_TrueI = thm "Eq_TrueI";
    26 val Ex1_def = thm "Ex1_def"
    27 val ex_disj_distrib = thm "ex_disj_distrib";
    28 val ex_simps = thms "ex_simps";
    29 val if_cancel = thm "if_cancel";
    30 val if_eq_cancel = thm "if_eq_cancel";
    31 val if_False = thm "if_False";
    32 val iff_conv_conj_imp = thm "iff_conv_conj_imp";
    33 val iff = thm "iff"
    34 val if_splits = thms "if_splits";
    35 val if_True = thm "if_True";
    36 val if_weak_cong = thm "if_weak_cong"
    37 val imp_all = thm "imp_all";
    38 val imp_cong = thm "imp_cong";
    39 val imp_conjL = thm "imp_conjL";
    40 val imp_conjR = thm "imp_conjR";
    41 val imp_conv_disj = thm "imp_conv_disj";
    42 val simp_implies_def = thm "simp_implies_def";
    43 val simp_thms = thms "simp_thms";
    44 val split_if = thm "split_if";
    45 val the1_equality = thm "the1_equality"
    46 val theI = thm "theI"
    47 val theI' = thm "theI'"
    48 val True_implies_equals = thm "True_implies_equals";