# HG changeset patch
# User oheimb
# Date 888418084 -3600
# Node ID 91af1ef45d68041c02ceed6aee7bd0f9721a8ac3
# Parent  89ad3eb863a15b72f4ed2506e3ae211088824829
added split_all_tac to claset()

diff -r 89ad3eb863a1 -r 91af1ef45d68 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Wed Feb 25 15:45:32 1998 +0100
+++ b/src/HOL/Prod.ML	Wed Feb 25 15:48:04 1998 +0100
@@ -80,9 +80,8 @@
 
 end;
 
-(* Could be nice, but breaks too many proofs:
-claset_ref() := claset() addbefore split_all_tac;
-*)
+(* consider addSbefore ?? *)
+claset_ref() := claset() addbefore ("split_all_tac",split_all_tac);
 
 (*** lemmas for splitting paired `!!'
 Does not work with simplifier because it also affects premises in
@@ -120,13 +119,13 @@
 ***)
 
 goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
-by (fast_tac (claset() addbefore split_all_tac) 1);
+by (Fast_tac 1);
 qed "split_paired_All";
 Addsimps [split_paired_All];
 (* AddIffs is not a good idea because it makes Blast_tac loop *)
 
 goal Prod.thy "(? x. P x) = (? a b. P(a,b))";
-by (fast_tac (claset() addbefore split_all_tac) 1);
+by (Fast_tac 1);
 qed "split_paired_Ex";
 Addsimps [split_paired_Ex];
 
diff -r 89ad3eb863a1 -r 91af1ef45d68 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Wed Feb 25 15:45:32 1998 +0100
+++ b/src/HOL/Relation.ML	Wed Feb 25 15:48:04 1998 +0100
@@ -215,11 +215,11 @@
     (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
 
 goal Relation.thy "R O id = R";
-by (fast_tac (claset() addbefore split_all_tac) 1);
+by (Fast_tac 1);
 qed "R_O_id";
 
 goal Relation.thy "id O R = R";
-by (fast_tac (claset() addbefore split_all_tac) 1);
+by (Fast_tac 1);
 qed "id_O_R";
 
 Addsimps [R_O_id,id_O_R];