changeset 58008 | aa72531f972f |
parent 56245 | 84fc7dfa3cd4 |
child 58009 | 987c848d509b |
--- 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;