src/HOL/HOL.thy
changeset 45654 cf10bde35973
parent 45625 750c5a47400b
child 46125 00cd193a48dc
     1.1 --- a/src/HOL/HOL.thy	Sun Nov 27 23:06:59 2011 +0100
     1.2 +++ b/src/HOL/HOL.thy	Sun Nov 27 23:10:19 2011 +0100
     1.3 @@ -2011,15 +2011,8 @@
     1.4    fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
     1.5  end;
     1.6  
     1.7 -val all_conj_distrib = @{thm all_conj_distrib};
     1.8 -val all_simps = @{thms all_simps};
     1.9 -val atomize_not = @{thm atomize_not};
    1.10  val case_split = @{thm case_split};
    1.11 -val cases_simp = @{thm cases_simp};
    1.12 -val choice_eq = @{thm choice_eq};
    1.13  val cong = @{thm cong};
    1.14 -val conj_comms = @{thms conj_comms};
    1.15 -val conj_cong = @{thm conj_cong};
    1.16  val de_Morgan_conj = @{thm de_Morgan_conj};
    1.17  val de_Morgan_disj = @{thm de_Morgan_disj};
    1.18  val disj_assoc = @{thm disj_assoc};
    1.19 @@ -2045,15 +2038,11 @@
    1.20  val imp_conjL = @{thm imp_conjL};
    1.21  val imp_conjR = @{thm imp_conjR};
    1.22  val imp_conv_disj = @{thm imp_conv_disj};
    1.23 -val simp_implies_def = @{thm simp_implies_def};
    1.24 -val simp_thms = @{thms simp_thms};
    1.25  val split_if = @{thm split_if};
    1.26  val the1_equality = @{thm the1_equality};
    1.27  val theI = @{thm theI};
    1.28  val theI' = @{thm theI'};
    1.29 -val True_implies_equals = @{thm True_implies_equals};
    1.30 -val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms @ @{thms "nnf_simps"})
    1.31 -
    1.32 +val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms nnf_simps});
    1.33  *}
    1.34  
    1.35  hide_const (open) eq equal