# HG changeset patch
# User oheimb
# Date 893698339 -7200
# Node ID 196100237656bb493e71b5d82e2ba122cbeb810c
# Parent  eab729051897623bf2b375b71ac158aea69d6fb5
cleanup for split_all_tac as wrapper in claset()

diff -r eab729051897 -r 196100237656 NEWS
--- a/NEWS	Mon Apr 27 19:30:40 1998 +0200
+++ b/NEWS	Mon Apr 27 19:32:19 1998 +0200
@@ -24,14 +24,16 @@
   combines rewriting and classical reasoning (and whatever other tools)
   similarly to auto_tac, but is aimed to solve the given subgoal totally.
 
-* added option_map_eq_Some to simpset(), option_map_eq_Some RS iffD1 to claset()
+* added option_map_eq_Some to simpset() and claset()
+
 * New directory HOL/UNITY: Chandy and Misra's UNITY formalism
 
 * split_all_tac is now much faster and fails if there is nothing to split.
   Existing (fragile) proofs may require adaption because the order and the
   names of the automatically generated variables have changed.
   split_all_tac has moved within claset() from usafe wrappers to safe wrappers,
-  which means that !!-bound variables are splitted much more aggressively.
+  which means that !!-bound variables are splitted much more aggressively,
+  and safe_tac and clarify_tac now split such variables.
   If this splitting is not appropriate, use delSWrapper "split_all_tac".
 
 * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset
diff -r eab729051897 -r 196100237656 src/HOL/IOA/Solve.ML
--- a/src/HOL/IOA/Solve.ML	Mon Apr 27 19:30:40 1998 +0200
+++ b/src/HOL/IOA/Solve.ML	Mon Apr 27 19:32:19 1998 +0200
@@ -74,7 +74,7 @@
 \    %i. fst (snd ex i))")]  bexI 1);
 (* fst(s) is in projected execution *)
  by (Simp_tac 1);
- by (fast_tac (claset() delWrapper"split_all_tac" delSWrapper"split_all_tac")1);
+ by (fast_tac (claset() delSWrapper"split_all_tac")1);
 (* projected execution is indeed an execution *)
 by (asm_full_simp_tac
       (simpset() addsimps [executions_def,is_execution_fragment_def,
@@ -94,7 +94,7 @@
 \    %i. snd (snd ex i))")]  bexI 1);
 (* fst(s) is in projected execution *)
  by (Simp_tac 1);
- by (fast_tac (claset() delWrapper"split_all_tac" delSWrapper"split_all_tac")1);
+ by (fast_tac (claset() delSWrapper"split_all_tac")1);
 (* projected execution is indeed an execution *)
 by (asm_full_simp_tac
       (simpset() addsimps [executions_def,is_execution_fragment_def,
diff -r eab729051897 -r 196100237656 src/HOL/Map.ML
--- a/src/HOL/Map.ML	Mon Apr 27 19:30:40 1998 +0200
+++ b/src/HOL/Map.ML	Mon Apr 27 19:32:19 1998 +0200
@@ -63,9 +63,8 @@
 goal thy "map_of xs k = Some y --> (k,y):set xs";
 by (list.induct_tac "xs" 1);
 by  (Simp_tac 1);
+by (split_all_tac 1);
 by (Asm_simp_tac 1);
-by (split_all_tac 1);
-by (Simp_tac 1);
 qed_spec_mp "map_of_SomeD";
 
 section "dom";
diff -r eab729051897 -r 196100237656 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Mon Apr 27 19:30:40 1998 +0200
+++ b/src/HOL/Trancl.ML	Mon Apr 27 19:32:19 1998 +0200
@@ -160,8 +160,7 @@
 qed "rtrancl_converseI";
 
 goal Trancl.thy "(r^-1)^* = (r^*)^-1";
-by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]
-			addSaltern ("split_all_tac", split_all_tac)));
+by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]));
 qed "rtrancl_converse";
 
 val major::prems = goal Trancl.thy
@@ -339,7 +338,7 @@
 
 
 goal Trancl.thy "(r^+)^= = r^*";
-by (safe_tac (claset() addSaltern ("split_all_tac", split_all_tac)));
+by Safe_tac;
 by  (etac trancl_into_rtrancl 1);
 by (etac rtranclE 1);
 by  (Auto_tac );
@@ -349,7 +348,7 @@
 Addsimps[reflcl_trancl];
 
 goal Trancl.thy "(r^=)^+ = r^*";
-by (safe_tac (claset() addSaltern ("split_all_tac", split_all_tac)));
+by Safe_tac;
 by  (dtac trancl_into_rtrancl 1);
 by  (Asm_full_simp_tac 1);
 by (etac rtranclE 1);