--- a/src/HOL/HOL.thy Mon Jan 09 14:47:18 2012 +0100
+++ b/src/HOL/HOL.thy Mon Jan 09 18:29:42 2012 +0100
@@ -2008,37 +2008,6 @@
fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
end;
-val case_split = @{thm case_split};
-val cong = @{thm cong};
-val de_Morgan_conj = @{thm de_Morgan_conj};
-val de_Morgan_disj = @{thm de_Morgan_disj};
-val disj_assoc = @{thm disj_assoc};
-val disj_comms = @{thms disj_comms};
-val disj_cong = @{thm disj_cong};
-val eq_ac = @{thms eq_ac};
-val eq_cong2 = @{thm eq_cong2}
-val Eq_FalseI = @{thm Eq_FalseI};
-val Eq_TrueI = @{thm Eq_TrueI};
-val Ex1_def = @{thm Ex1_def};
-val ex_disj_distrib = @{thm ex_disj_distrib};
-val ex_simps = @{thms ex_simps};
-val if_cancel = @{thm if_cancel};
-val if_eq_cancel = @{thm if_eq_cancel};
-val if_False = @{thm if_False};
-val iff_conv_conj_imp = @{thm iff_conv_conj_imp};
-val iff = @{thm iff};
-val if_splits = @{thms if_splits};
-val if_True = @{thm if_True};
-val if_weak_cong = @{thm if_weak_cong};
-val imp_all = @{thm imp_all};
-val imp_cong = @{thm imp_cong};
-val imp_conjL = @{thm imp_conjL};
-val imp_conjR = @{thm imp_conjR};
-val imp_conv_disj = @{thm imp_conv_disj};
-val split_if = @{thm split_if};
-val the1_equality = @{thm the1_equality};
-val theI = @{thm theI};
-val theI' = @{thm theI'};
val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms nnf_simps});
*}