# HG changeset patch
# User oheimb
# Date 849026965 -3600
# Node ID 041bf27011b1d95d43f2dc6fb47d86b06cd63ef7
# Parent  f919bdd5f9b6321cc6448034e4404329eee0a0e1
if_cancel added to HOL_ss

diff -r f919bdd5f9b6 -r 041bf27011b1 src/HOL/simpdata.ML
--- 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];