# HG changeset patch
# User oheimb
# Date 879334215 -3600
# Node ID 96632970d20361dbd73d068cdea6a6001be6fdd0
# Parent  7b15e7eee9823fed2a44bc5ae5e700f405eb9de8
simpdata.ML: renamed split_prem_tac to split_asm_tac, added split_if_asm
cladata.ML: unintentinally committed

diff -r 7b15e7eee982 -r 96632970d203 src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Wed Nov 12 12:24:55 1997 +0100
+++ b/src/HOL/cladata.ML	Wed Nov 12 12:30:15 1997 +0100
@@ -26,6 +26,9 @@
 structure Hypsubst = HypsubstFun(Hypsubst_Data);
 open Hypsubst;
 
+val thin_refl = prove_goal HOL.thy 
+	"!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
+
 (*** Applying ClassicalFun to create a classical prover ***)
 structure Classical_Data = 
   struct
@@ -33,7 +36,8 @@
   val mp        = mp
   val not_elim  = notE
   val classical = classical
-  val hyp_subst_tacs=[hyp_subst_tac]
+  val thin_refl = thin_refl
+  val hyp_subst_tacs= [REPEAT_DETERM o ematch_tac [thin_refl] THEN' hyp_subst_tac]
   end;
 
 structure Classical = ClassicalFun(Classical_Data);
diff -r 7b15e7eee982 -r 96632970d203 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Nov 12 12:24:55 1997 +0100
+++ b/src/HOL/simpdata.ML	Wed Nov 12 12:30:15 1997 +0100
@@ -340,11 +340,16 @@
  (fn _ => [blast_tac (HOL_cs addIs [select_equality]) 1]);
 
 qed_goal "expand_if" HOL.thy
-    "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
- (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),
+    "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" (K [
+	res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1,
          stac if_P 2,
          stac if_not_P 1,
-         REPEAT(blast_tac HOL_cs 1) ]);
+         ALLGOALS (blast_tac HOL_cs)]);
+
+qed_goal "split_if_asm" HOL.thy
+    "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))" (K [
+	stac expand_if 1,
+        blast_tac HOL_cs 1]);
 
 qed_goal "if_bool_eq" HOL.thy
                    "(if P then Q else R) = ((P-->Q) & (~P-->R))"
@@ -364,8 +369,8 @@
 fun split_inside_tac splits = mktac (map mk_meta_eq splits)
 end;
 
-val split_prem_tac = mk_case_split_prem_tac split_tac disjE conjE exE contrapos
-					    contrapos2 notnotD;
+val split_asm_tac = mk_case_split_asm_tac split_tac 
+			(disjE,conjE,exE,contrapos,contrapos2,notnotD);
 
 infix 4 addsplits;
 fun ss addsplits splits = ss addloop (split_tac splits);