# HG changeset patch
# User wenzelm
# Date 1408460444 -7200
# Node ID aa72531f972f1fdcc4dd30a913cc07baf8007bf9
# Parent  671c607fb4af5a384ecba7f49f9e08eed2a2b12e
added PARALLEL_ALLGOALS convenience;

diff -r 671c607fb4af -r aa72531f972f NEWS
--- 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)
 ---------------------------------
diff -r 671c607fb4af -r aa72531f972f src/Provers/clasimp.ML
--- 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
diff -r 671c607fb4af -r aa72531f972f src/Pure/goal.ML
--- 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;
diff -r 671c607fb4af -r aa72531f972f src/Pure/simplifier.ML
--- 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 =>