# HG changeset patch
# User oheimb
# Date 891949387 -7200
# Node ID 82b0ed20c2cbf2c1f0982ca42a3417de5cf75701
# Parent  7cfc85fc6fd701164e44ea23f947e030c51ee272
made split_all_tac as safe wrapper more defensive:
if it is added as unsafe wrapper again (as its was before),
this does not break the current proofs.

diff -r 7cfc85fc6fd7 -r 82b0ed20c2cb src/HOL/IOA/IOA.ML
--- a/src/HOL/IOA/IOA.ML	Sat Apr 04 14:30:19 1998 +0200
+++ b/src/HOL/IOA/IOA.ML	Tue Apr 07 13:43:07 1998 +0200
@@ -55,7 +55,7 @@
 goalw IOA.thy (reachable_def::exec_rws)
 "!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t";
   by (asm_full_simp_tac (simpset() delsimps bex_simps) 1);
-  by Safe_tac;
+  by (safe_tac (claset() addSaltern ("split_all_tac", split_all_tac)));
   by (rename_tac "n ex1 ex2 a1 a4 a5 a2 a3" 1);
   by (res_inst_tac [("x","(%i. if i<n then ex1 i                    \
 \                            else (if i=n then Some a else None),    \
@@ -78,7 +78,7 @@
 \     !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \
 \  ==> invariant A P";
   by (rewrite_goals_tac(reachable_def::Let_def::exec_rws));
-  by Safe_tac;
+  by (safe_tac (claset() addSaltern ("split_all_tac", split_all_tac)));
   by (rename_tac "n ex1 ex2" 1);
   by (res_inst_tac [("Q","reachable A (ex2 n)")] conjunct1 1);
   by (Asm_full_simp_tac 1);
diff -r 7cfc85fc6fd7 -r 82b0ed20c2cb src/HOL/IOA/Solve.ML
--- a/src/HOL/IOA/Solve.ML	Sat Apr 04 14:30:19 1998 +0200
+++ b/src/HOL/IOA/Solve.ML	Tue Apr 07 13:43:07 1998 +0200
@@ -15,7 +15,7 @@
 \          is_weak_pmap f C A |] ==> traces(C) <= traces(A)";
 
   by (simp_tac(simpset() addsimps [has_trace_def])1);
-  by Safe_tac;
+  by (safe_tac (claset() addSaltern ("split_all_tac", split_all_tac)));
   by (rename_tac "f ex1 ex2" 1);
 
   (* choose same trace, therefore same NF *)
@@ -74,12 +74,12 @@
 \    %i. fst (snd ex i))")]  bexI 1);
 (* fst(s) is in projected execution *)
  by (Simp_tac 1);
- by (fast_tac (claset() delSWrapper "split_all_tac") 1);
+ by (fast_tac (claset() delWrapper"split_all_tac" delSWrapper"split_all_tac")1);
 (* projected execution is indeed an execution *)
 by (asm_full_simp_tac
       (simpset() addsimps [executions_def,is_execution_fragment_def,
                           par_def,starts_of_def,trans_of_def,filter_oseq_def]
-                addsplits [expand_if,split_option_case]) 1);
+                addsplits [split_option_case]) 1);
 qed"comp1_reachable";
 
 
@@ -94,12 +94,12 @@
 \    %i. snd (snd ex i))")]  bexI 1);
 (* fst(s) is in projected execution *)
  by (Simp_tac 1);
- by (fast_tac (claset() delSWrapper "split_all_tac") 1);
+ by (fast_tac (claset() delWrapper"split_all_tac" delSWrapper"split_all_tac")1);
 (* projected execution is indeed an execution *)
 by (asm_full_simp_tac
       (simpset() addsimps [executions_def,is_execution_fragment_def,
                           par_def,starts_of_def,trans_of_def,filter_oseq_def]
-                addsplits [expand_if,split_option_case]) 1);
+                addsplits [split_option_case]) 1);
 qed"comp2_reachable";
 
 Delsplits [expand_if];
diff -r 7cfc85fc6fd7 -r 82b0ed20c2cb src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Sat Apr 04 14:30:19 1998 +0200
+++ b/src/HOL/Prod.ML	Tue Apr 07 13:43:07 1998 +0200
@@ -80,7 +80,8 @@
 
 end;
 
-claset_ref() := claset() addSaltern ("split_all_tac", split_all_tac);
+(* claset_ref() := claset() addbefore  ("split_all_tac", TRY o split_all_tac);*)
+   claset_ref() := claset() addSaltern ("split_all_tac",       split_all_tac);
 
 (*** lemmas for splitting paired `!!'
 Does not work with simplifier because it also affects premises in
@@ -173,7 +174,7 @@
 qed "expand_split";
 
 (* could be done after split_tac has been speeded up significantly:
-simpset_ref() := (simpset() addsplits [expand_split]);
+simpset_ref() := simpset() addsplits [expand_split];
    precompute the constants involved and don't do anything unless
    the current goal contains one of those constants
 *)
diff -r 7cfc85fc6fd7 -r 82b0ed20c2cb src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Sat Apr 04 14:30:19 1998 +0200
+++ b/src/HOL/Trancl.ML	Tue Apr 07 13:43:07 1998 +0200
@@ -153,7 +153,8 @@
 qed "rtrancl_converseI";
 
 goal Trancl.thy "(r^-1)^* = (r^*)^-1";
-by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]));
+by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]
+			addSaltern ("split_all_tac", split_all_tac)));
 qed "rtrancl_converse";
 
 val major::prems = goal Trancl.thy
@@ -331,7 +332,7 @@
 
 
 goal Trancl.thy "(r^+)^= = r^*";
-by Safe_tac;
+by (safe_tac (claset() addSaltern ("split_all_tac", split_all_tac)));
 by  (etac trancl_into_rtrancl 1);
 by (etac rtranclE 1);
 by  (Auto_tac );
@@ -341,7 +342,7 @@
 Addsimps[reflcl_trancl];
 
 goal Trancl.thy "(r^=)^+ = r^*";
-by Safe_tac;
+by (safe_tac (claset() addSaltern ("split_all_tac", split_all_tac)));
 by  (dtac trancl_into_rtrancl 1);
 by  (Asm_full_simp_tac 1);
 by (etac rtranclE 1);