1.1 --- a/src/HOL/HOL.thy	Mon Jan 09 14:47:18 2012 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Jan 09 18:29:42 2012 +0100
     1.3 @@ -2008,37 +2008,6 @@
     1.4    fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
     1.5  end;
     1.6  
     1.7 -val case_split = @{thm case_split};
     1.8 -val cong = @{thm cong};
     1.9 -val de_Morgan_conj = @{thm de_Morgan_conj};
    1.10 -val de_Morgan_disj = @{thm de_Morgan_disj};
    1.11 -val disj_assoc = @{thm disj_assoc};
    1.12 -val disj_comms = @{thms disj_comms};
    1.13 -val disj_cong = @{thm disj_cong};
    1.14 -val eq_ac = @{thms eq_ac};
    1.15 -val eq_cong2 = @{thm eq_cong2}
    1.16 -val Eq_FalseI = @{thm Eq_FalseI};
    1.17 -val Eq_TrueI = @{thm Eq_TrueI};
    1.18 -val Ex1_def = @{thm Ex1_def};
    1.19 -val ex_disj_distrib = @{thm ex_disj_distrib};
    1.20 -val ex_simps = @{thms ex_simps};
    1.21 -val if_cancel = @{thm if_cancel};
    1.22 -val if_eq_cancel = @{thm if_eq_cancel};
    1.23 -val if_False = @{thm if_False};
    1.24 -val iff_conv_conj_imp = @{thm iff_conv_conj_imp};
    1.25 -val iff = @{thm iff};
    1.26 -val if_splits = @{thms if_splits};
    1.27 -val if_True = @{thm if_True};
    1.28 -val if_weak_cong = @{thm if_weak_cong};
    1.29 -val imp_all = @{thm imp_all};
    1.30 -val imp_cong = @{thm imp_cong};
    1.31 -val imp_conjL = @{thm imp_conjL};
    1.32 -val imp_conjR = @{thm imp_conjR};
    1.33 -val imp_conv_disj = @{thm imp_conv_disj};
    1.34 -val split_if = @{thm split_if};
    1.35 -val the1_equality = @{thm the1_equality};
    1.36 -val theI = @{thm theI};
    1.37 -val theI' = @{thm theI'};
    1.38  val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms nnf_simps});
    1.39  *}
    1.40