support structural composition (THEN_ALL_NEW) for proof methods;
clarified preparation for goal restriction: Goal.conjunction_tac only once;
export Method.parse0, notably for Eisbach;
more explicit type cases_state;

--- a/NEWS	Mon Mar 09 11:32:32 2015 +0100
+++ b/NEWS	Mon Mar 09 20:33:33 2015 +0100
@@ -6,6 +6,9 @@
 
 *** General ***
 
+* Structural composition of proof methods (meth1; meth2) in Isar
+corresponds to (tac1 THEN_ALL_NEW tac2) in ML.
+
 * Generated schematic variables in standard format of exported facts are
 incremented to avoid material in the proof context. Rare
 INCOMPATIBILITY, explicit instantiation sometimes needs to refer to

--- a/src/Doc/Isar_Ref/Proof.thy	Mon Mar 09 11:32:32 2015 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy	Mon Mar 09 20:33:33 2015 +0100
@@ -531,38 +531,54 @@
 
 subsection \<open>Proof method expressions \label{sec:proof-meth}\<close>
 
-text \<open>Proof methods are either basic ones, or expressions composed
-  of methods via ``@{verbatim ","}'' (sequential composition),
-  ``@{verbatim "|"}'' (alternative choices), ``@{verbatim "?"}''
-  (try), ``@{verbatim "+"}'' (repeat at least once), ``@{verbatim
-  "["}@{text n}@{verbatim "]"}'' (restriction to first @{text n}
-  sub-goals, with default @{text "n = 1"}).  In practice, proof
-  methods are usually just a comma separated list of @{syntax
-  nameref}~@{syntax args} specifications.  Note that parentheses may
-  be dropped for single method specifications (with no arguments).
+text \<open>Proof methods are either basic ones, or expressions composed of
+  methods via ``@{verbatim ","}'' (sequential composition), ``@{verbatim
+  ";"}'' (structural composition), ``@{verbatim "|"}'' (alternative
+  choices), ``@{verbatim "?"}'' (try), ``@{verbatim "+"}'' (repeat at least
+  once), ``@{verbatim "["}@{text n}@{verbatim "]"}'' (restriction to first
+  @{text n} subgoals). In practice, proof methods are usually just a comma
+  separated list of @{syntax nameref}~@{syntax args} specifications. Note
+  that parentheses may be dropped for single method specifications (with no
+  arguments). The syntactic precedence of method combinators is @{verbatim
+  "|"} @{verbatim ";"} @{verbatim ","} @{verbatim "[]"} @{verbatim "+"}
+  @{verbatim "?"} (from low to high).
 
   @{rail \<open>
     @{syntax_def method}:
       (@{syntax nameref} | '(' methods ')') (() | '?' | '+' | '[' @{syntax nat}? ']')
     ;
-    methods: (@{syntax nameref} @{syntax args} | @{syntax method}) + (',' | '|')
+    methods: (@{syntax nameref} @{syntax args} | @{syntax method}) + (',' | ';' | '|')
   \<close>}
 
-  Proper Isar proof methods do \emph{not} admit arbitrary goal
-  addressing, but refer either to the first sub-goal or all sub-goals
-  uniformly.  The goal restriction operator ``@{text "[n]"}''
-  evaluates a method expression within a sandbox consisting of the
-  first @{text n} sub-goals (which need to exist).  For example, the
-  method ``@{text "simp_all[3]"}'' simplifies the first three
-  sub-goals, while ``@{text "(rule foo, simp_all)[]"}'' simplifies all
-  new goals that emerge from applying rule @{text "foo"} to the
-  originally first one.
+  Regular Isar proof methods do \emph{not} admit direct goal addressing, but
+  refer to the first subgoal or to all subgoals uniformly. Nonetheless,
+  the subsequent mechanisms allow to imitate the effect of subgoal
+  addressing that is known from ML tactics.
+
+  \medskip Goal \emph{restriction} means the proof state is wrapped-up in a
+  way that certain subgoals are exposed, and other subgoals are ``parked''
+  elsewhere. Thus a proof method has no other chance than to operate on the
+  subgoals that are presently exposed.
 
-  Improper methods, notably tactic emulations, offer a separate
-  low-level goal addressing scheme as explicit argument to the
-  individual tactic being involved.  Here ``@{text "[!]"}'' refers to
-  all goals, and ``@{text "[n-]"}'' to all goals starting from @{text
-  "n"}.
+  Structural composition ``@{text m\<^sub>1}@{verbatim ";"}~@{text m\<^sub>2}'' means
+  that method @{text m\<^sub>1} is applied with restriction to the first subgoal,
+  then @{text m\<^sub>2} is applied consecutively with restriction to each subgoal
+  that has newly emerged due to @{text m\<^sub>1}. This is analogous to the tactic
+  combinator @{ML THEN_ALL_NEW} in Isabelle/ML, see also @{cite
+  "isabelle-implementation"}. For example, @{text "(rule r; blast)"} applies
+  rule @{text "r"} and then solves all new subgoals by @{text blast}.
+
+  Moreover, the explicit goal restriction operator ``@{text "[n]"}'' exposes
+  only the first @{text n} subgoals (which need to exist), with default
+  @{text "n = 1"}. For example, the method expression ``@{text
+  "simp_all[3]"}'' simplifies the first three subgoals, while ``@{text
+  "(rule r, simp_all)[]"}'' simplifies all new goals that emerge from
+  applying rule @{text "r"} to the originally first one.
+
+  \medskip Improper methods, notably tactic emulations, offer low-level goal
+  addressing as explicit argument to the individual tactic being involved.
+  Here ``@{text "[!]"}'' refers to all goals, and ``@{text "[n-]"}'' to all
+  goals starting from @{text "n"}.
 
   @{rail \<open>
     @{syntax_def goal_spec}:

--- a/src/Pure/Isar/method.ML	Mon Mar 09 11:32:32 2015 +0100
+++ b/src/Pure/Isar/method.ML	Mon Mar 09 20:33:33 2015 +0100
@@ -41,7 +41,7 @@
   val set_tactic: (morphism -> thm list -> tactic) -> Context.generic -> Context.generic
   type combinator_info
   val no_combinator_info: combinator_info
-  datatype combinator = Then | Orelse | Try | Repeat1 | Select_Goals of int
+  datatype combinator = Then | Then_All_New | Orelse | Try | Repeat1 | Select_Goals of int
   datatype text =
     Source of Token.src |
     Basic of Proof.context -> method |
@@ -75,6 +75,7 @@
   val position: text_range option -> Position.T
   val reports_of: text_range -> Position.report list
   val report: text_range -> unit
+  val parse0: text_range parser
   val parse: text_range parser
 end;
 
@@ -299,7 +300,7 @@
 fun combinator_info keywords = Combinator_Info {keywords = keywords};
 val no_combinator_info = combinator_info [];
 
-datatype combinator = Then | Orelse | Try | Repeat1 | Select_Goals of int;
+datatype combinator = Then | Then_All_New | Orelse | Try | Repeat1 | Select_Goals of int;
 
 datatype text =
   Source of Token.src |
@@ -408,28 +409,40 @@
 
 local
 
-fun APPEND_CASES (meth: cases_tactic) (cases, st) =
-  meth st |> Seq.map (fn (cases', st') => (cases @ cases', st'));
+fun APPEND_CASES (tac: cases_tactic) ((cases, st): cases_state) =
+  tac st |> Seq.map (fn (cases', st') => (cases @ cases', st'));
 
-fun BYPASS_CASES (tac: tactic) (cases, st) =
+fun BYPASS_CASES (tac: tactic) ((cases, st): cases_state) =
   tac st |> Seq.map (pair cases);
 
 val op THEN = Seq.THEN;
 
-fun SELECT_GOALS n method =
-  BYPASS_CASES
-    (ALLGOALS Goal.conjunction_tac THEN PRIMITIVE (Goal.restrict 1 n) THEN Goal.conjunction_tac 1)
-  THEN method
-  THEN BYPASS_CASES (PRIMITIVE (Goal.unrestrict 1));
+val preparation = BYPASS_CASES (ALLGOALS Goal.conjunction_tac);
+
+fun RESTRICT_GOAL i n method =
+  BYPASS_CASES (PRIMITIVE (Goal.restrict i n)) THEN
+  method THEN
+  BYPASS_CASES (PRIMITIVE (Goal.unrestrict i));
+
+fun SELECT_GOAL method i = RESTRICT_GOAL i 1 method;
+
+fun (method1 THEN_ALL_NEW method2) i (st: cases_state) =
+  st |> (method1 i THEN (fn st' =>
+    Seq.INTERVAL method2 i (i + Thm.nprems_of (snd st') - Thm.nprems_of (snd st)) st'));
 
 fun COMBINATOR1 comb [meth] = comb meth
   | COMBINATOR1 _ _ = raise Fail "Method combinator requires exactly one argument";
 
 fun combinator Then = Seq.EVERY
+  | combinator Then_All_New =
+      (fn [] => Seq.single
+        | methods =>
+            preparation THEN foldl1 (op THEN_ALL_NEW) (map SELECT_GOAL methods) 1)
   | combinator Orelse = Seq.FIRST
   | combinator Try = COMBINATOR1 Seq.TRY
   | combinator Repeat1 = COMBINATOR1 Seq.REPEAT1
-  | combinator (Select_Goals n) = COMBINATOR1 (SELECT_GOALS n);
+  | combinator (Select_Goals n) =
+      COMBINATOR1 (fn method => preparation THEN RESTRICT_GOAL 1 n method);
 
 in
 
@@ -548,35 +561,38 @@
 
 local
 
-fun meth4 x =
+fun meth5 x =
  (Parse.position Parse.xname >> (fn name => Source (Token.src name [])) ||
   Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok =>
     Source (Token.src ("cartouche", Token.pos_of tok) [tok])) ||
   Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
-and meth3 x =
- (meth4 -- Parse.position (Parse.$$$ "?")
+and meth4 x =
+ (meth5 -- Parse.position (Parse.$$$ "?")
     >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Try, [m])) ||
-  meth4 -- Parse.position (Parse.$$$ "+")
+  meth5 -- Parse.position (Parse.$$$ "+")
     >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Repeat1, [m])) ||
-  meth4 --
+  meth5 --
     (Parse.position (Parse.$$$ "[") -- Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]"))
     >> (fn (m, (((_, pos1), n), (_, pos2))) =>
         Combinator (combinator_info [pos1, pos2], Select_Goals n, [m])) ||
+  meth5) x
+and meth3 x =
+ (Parse.position Parse.xname -- Parse.args1 is_symid_meth >> (Source o uncurry Token.src) ||
   meth4) x
 and meth2 x =
- (Parse.position Parse.xname -- Parse.args1 is_symid_meth >> (Source o uncurry Token.src) ||
-  meth3) x
+  (Parse.enum1_positions "," meth3
+    >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then, ms))) x
 and meth1 x =
-  (Parse.enum1_positions "," meth2
-    >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then, ms))) x
+  (Parse.enum1_positions ";" meth2
+    >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then_All_New, ms))) x
 and meth0 x =
   (Parse.enum1_positions "|" meth1
     >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Orelse, ms))) x;
 
 in
 
-val parse =
-  Scan.trace meth3 >> (fn (m, toks) => (m, Token.range_of toks));
+val parse0 = Scan.trace meth0 >> (fn (m, toks) => (m, Token.range_of toks));
+val parse = Scan.trace meth4 >> (fn (m, toks) => (m, Token.range_of toks));
 
 end;
 

--- a/src/Pure/Isar/rule_cases.ML	Mon Mar 09 11:32:32 2015 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Mon Mar 09 20:33:33 2015 +0100
@@ -9,7 +9,8 @@
 signature BASIC_RULE_CASES =
 sig
   type cases
-  type cases_tactic
+  type cases_state = cases * thm
+  type cases_tactic = thm -> cases_state Seq.seq
   val CASES: cases -> tactic -> cases_tactic
   val NO_CASES: tactic -> cases_tactic
   val SUBGOAL_CASES: ((term * int * thm) -> cases_tactic) -> int -> cases_tactic
@@ -183,7 +184,8 @@
 
 (** tactics with cases **)
 
-type cases_tactic = thm -> (cases * thm) Seq.seq;
+type cases_state = cases * thm;
+type cases_tactic = thm -> cases_state Seq.seq;
 
 fun CASES cases tac st = Seq.map (pair cases) (tac st);
 fun NO_CASES tac = CASES [] tac;

--- a/src/Pure/tactical.ML	Mon Mar 09 11:32:32 2015 +0100
+++ b/src/Pure/tactical.ML	Mon Mar 09 20:33:33 2015 +0100
@@ -351,7 +351,8 @@
 (*Apply second tactic to all subgoals emerging from the first --
   following usual convention for subgoal-based tactics.*)
 fun (tac1 THEN_ALL_NEW tac2) i st =
-  st |> (tac1 i THEN (fn st' => Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st) st'));
+  st |> (tac1 i THEN (fn st' =>
+    Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st) st'));
 
 (*Repeatedly dig into any emerging subgoals.*)
 fun REPEAT_ALL_NEW tac =