src/HOL/HOL.thy
changeset 22839 ede26eb5e549
parent 22744 5cbe966d67a2
child 22993 838c66e760b5
     1.1 --- a/src/HOL/HOL.thy	Sun May 06 21:49:23 2007 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sun May 06 21:49:24 2007 +0200
     1.3 @@ -40,10 +40,10 @@
     1.4    Ex1           :: "('a => bool) => bool"           (binder "EX! " 10)
     1.5    Let           :: "['a, 'a => 'b] => 'b"
     1.6  
     1.7 -  "="           :: "['a, 'a] => bool"               (infixl 50)
     1.8 -  &             :: "[bool, bool] => bool"           (infixr 35)
     1.9 -  "|"           :: "[bool, bool] => bool"           (infixr 30)
    1.10 -  -->           :: "[bool, bool] => bool"           (infixr 25)
    1.11 +  "op ="        :: "['a, 'a] => bool"               (infixl "=" 50)
    1.12 +  "op &"        :: "[bool, bool] => bool"           (infixr "&" 35)
    1.13 +  "op |"        :: "[bool, bool] => bool"           (infixr "|" 30)
    1.14 +  "op -->"      :: "[bool, bool] => bool"           (infixr "-->" 25)
    1.15  
    1.16  local
    1.17  
    1.18 @@ -1463,7 +1463,7 @@
    1.19  *}
    1.20  
    1.21  
    1.22 -subsection {* Legacy tactics *}
    1.23 +subsection {* Legacy tactics and ML bindings *}
    1.24  
    1.25  ML {*
    1.26  fun strip_tac i = REPEAT (resolve_tac [impI, allI] i);
    1.27 @@ -1478,6 +1478,49 @@
    1.28    fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
    1.29    fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
    1.30  end;
    1.31 +
    1.32 +val all_conj_distrib = thm "all_conj_distrib";
    1.33 +val all_simps = thms "all_simps";
    1.34 +val atomize_not = thm "atomize_not";
    1.35 +val case_split = thm "case_split_thm";
    1.36 +val case_split_thm = thm "case_split_thm"
    1.37 +val cases_simp = thm "cases_simp";
    1.38 +val choice_eq = thm "choice_eq"
    1.39 +val cong = thm "cong"
    1.40 +val conj_comms = thms "conj_comms";
    1.41 +val conj_cong = thm "conj_cong";
    1.42 +val de_Morgan_conj = thm "de_Morgan_conj";
    1.43 +val de_Morgan_disj = thm "de_Morgan_disj";
    1.44 +val disj_assoc = thm "disj_assoc";
    1.45 +val disj_comms = thms "disj_comms";
    1.46 +val disj_cong = thm "disj_cong";
    1.47 +val eq_ac = thms "eq_ac";
    1.48 +val eq_cong2 = thm "eq_cong2"
    1.49 +val Eq_FalseI = thm "Eq_FalseI";
    1.50 +val Eq_TrueI = thm "Eq_TrueI";
    1.51 +val Ex1_def = thm "Ex1_def"
    1.52 +val ex_disj_distrib = thm "ex_disj_distrib";
    1.53 +val ex_simps = thms "ex_simps";
    1.54 +val if_cancel = thm "if_cancel";
    1.55 +val if_eq_cancel = thm "if_eq_cancel";
    1.56 +val if_False = thm "if_False";
    1.57 +val iff_conv_conj_imp = thm "iff_conv_conj_imp";
    1.58 +val iff = thm "iff"
    1.59 +val if_splits = thms "if_splits";
    1.60 +val if_True = thm "if_True";
    1.61 +val if_weak_cong = thm "if_weak_cong"
    1.62 +val imp_all = thm "imp_all";
    1.63 +val imp_cong = thm "imp_cong";
    1.64 +val imp_conjL = thm "imp_conjL";
    1.65 +val imp_conjR = thm "imp_conjR";
    1.66 +val imp_conv_disj = thm "imp_conv_disj";
    1.67 +val simp_implies_def = thm "simp_implies_def";
    1.68 +val simp_thms = thms "simp_thms";
    1.69 +val split_if = thm "split_if";
    1.70 +val the1_equality = thm "the1_equality"
    1.71 +val theI = thm "theI"
    1.72 +val theI' = thm "theI'"
    1.73 +val True_implies_equals = thm "True_implies_equals";
    1.74  *}
    1.75  
    1.76  end