--- a/NEWS Tue Aug 19 16:46:07 2014 +0200
+++ b/NEWS Tue Aug 19 17:00:44 2014 +0200
@@ -23,6 +23,12 @@
min
+*** ML ***
+
+* Tactical PARALLEL_ALLGOALS is the most common way to refer to
+PARALLEL_GOALS.
+
+
New in Isabelle2014 (August 2014)
---------------------------------
--- a/src/Provers/clasimp.ML Tue Aug 19 16:46:07 2014 +0200
+++ b/src/Provers/clasimp.ML Tue Aug 19 17:00:44 2014 +0200
@@ -146,7 +146,7 @@
ORELSE'
(CHANGED o nodup_depth_tac (addss ctxt) n); (* slower but more general *)
in
- PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac ctxt)) THEN
+ PARALLEL_ALLGOALS (Simplifier.asm_full_simp_tac ctxt) THEN
TRY (Classical.safe_tac ctxt) THEN
REPEAT_DETERM (FIRSTGOAL main_tac) THEN
TRY (Classical.safe_tac (addSss ctxt)) THEN
--- a/src/Pure/goal.ML Tue Aug 19 16:46:07 2014 +0200
+++ b/src/Pure/goal.ML Tue Aug 19 17:00:44 2014 +0200
@@ -13,6 +13,7 @@
val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
val PARALLEL_CHOICE: tactic list -> tactic
val PARALLEL_GOALS: tactic -> tactic
+ val PARALLEL_ALLGOALS: (int -> tactic) -> tactic
end;
signature GOAL =
@@ -384,6 +385,8 @@
end;
+val PARALLEL_ALLGOALS = PARALLEL_GOALS o ALLGOALS;
+
end;
structure Basic_Goal: BASIC_GOAL = Goal;
--- a/src/Pure/simplifier.ML Tue Aug 19 16:46:07 2014 +0200
+++ b/src/Pure/simplifier.ML Tue Aug 19 17:00:44 2014 +0200
@@ -374,7 +374,7 @@
Method.setup @{binding simp_all}
(simp_method more_mods (fn ctxt => fn tac => fn facts =>
ALLGOALS (Method.insert_tac facts) THEN
- (CHANGED_PROP o PARALLEL_GOALS o ALLGOALS o tac) ctxt))
+ (CHANGED_PROP o PARALLEL_ALLGOALS o tac) ctxt))
"simplification (all goals)";
fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn ctxt0 =>