# HG changeset patch
# User oheimb
# Date 849099109 -3600
# Node ID e0e3836f333ddb3a42c5e9504cbc0caa6feef83e
# Parent  891eb76b8045cf2b44a816cba330342d9fc1a2b6
moved if_cancel to the right place

diff -r 891eb76b8045 -r e0e3836f333d src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Nov 27 13:13:21 1996 +0100
+++ b/src/HOL/simpdata.ML	Wed Nov 27 13:51:49 1996 +0100
@@ -262,6 +262,9 @@
                    "(if P then Q else R) = ((P-->Q) & (~P-->R))"
                    (fn _ => [rtac expand_if 1]);
 
+qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
+  (fn _ => [split_tac [expand_if] 1, fast_tac HOL_cs 1]);
+
 (** 'if' congruence rules: neither included by default! *)
 
 (*Simplifies x assuming c and y assuming ~c*)
@@ -298,7 +301,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];
@@ -315,9 +319,6 @@
 end;
 
 
-qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
-  (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
-
 qed_goal "if_distrib" HOL.thy
   "f(if c then x else y) = (if c then f x else f y)" 
   (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
@@ -330,7 +331,7 @@
 
 (*** Install simpsets and datatypes in theory structure ***)
 
-simpset := HOL_ss addsimps [if_cancel];
+simpset := HOL_ss;
 
 exception SS_DATA of simpset;