--- 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
--- 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,
--- 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";
--- 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);