# HG changeset patch
# User oheimb
# Date 849096801 -3600
# Node ID 891eb76b8045cf2b44a816cba330342d9fc1a2b6
# Parent  2af17dd5479e79daaf84caee08deec9f0211374c
added if_cancel later to simpset

diff -r 2af17dd5479e -r 891eb76b8045 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Nov 27 13:04:04 1996 +0100
+++ b/src/HOL/simpdata.ML	Wed Nov 27 13:13:21 1996 +0100
@@ -298,8 +298,7 @@
       setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
                              ORELSE' etac FalseE)
       setsubgoaler asm_simp_tac
-      addsimps ([if_True, if_False, if_cancel,
-		 o_apply, imp_disjL, conj_assoc, disj_assoc,
+      addsimps ([if_True, if_False, 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];
@@ -331,7 +330,7 @@
 
 (*** Install simpsets and datatypes in theory structure ***)
 
-simpset := HOL_ss;
+simpset := HOL_ss addsimps [if_cancel];
 
 exception SS_DATA of simpset;