--- a/src/HOL/simpdata.ML Tue Nov 26 16:57:13 1996 +0100
+++ b/src/HOL/simpdata.ML Tue Nov 26 17:49:25 1996 +0100
@@ -298,7 +298,8 @@
setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
ORELSE' etac FalseE)
setsubgoaler asm_simp_tac
- addsimps ([if_True, if_False, o_apply, imp_disjL, conj_assoc, disj_assoc,
+ addsimps ([if_True, if_False, if_cancel,
+ o_apply, imp_disjL, conj_assoc, disj_assoc,
de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp]
@ ex_simps @ all_simps @ simp_thms)
addcongs [imp_cong];