--- a/NEWS Tue Aug 13 15:34:46 2019 +0200
+++ b/NEWS Tue Aug 13 20:16:03 2019 +0200
@@ -9,6 +9,15 @@
New in this Isabelle version
----------------------------
+*** Isar ***
+
+* The proof method combinator (subproofs m) applies the method
+expression m consecutively to each subgoal, constructing individual
+subproofs internally. This impacts the internal construction of proof
+terms: it makes a cascade of let-expressions within the derivation tree
+and may thus improve scalability.
+
+
*** HOL ***
* ASCII membership syntax concerning big operators for infimum
--- a/src/Doc/Isar_Ref/Proof.thy Tue Aug 13 15:34:46 2019 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Tue Aug 13 20:16:03 2019 +0200
@@ -766,6 +766,7 @@
@{command_def "print_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\[0.5ex]
@{method_def "-"} & : & \<open>method\<close> \\
@{method_def "goal_cases"} & : & \<open>method\<close> \\
+ @{method_def "subproofs"} & : & \<open>method\<close> \\
@{method_def "fact"} & : & \<open>method\<close> \\
@{method_def "assumption"} & : & \<open>method\<close> \\
@{method_def "this"} & : & \<open>method\<close> \\
@@ -782,6 +783,8 @@
\<^rail>\<open>
@@{method goal_cases} (@{syntax name}*)
;
+ @@{method subproofs} @{syntax method}
+ ;
@@{method fact} @{syntax thms}?
;
@@{method (Pure) rule} @{syntax thms}?
@@ -825,6 +828,14 @@
premises, and @{command let} variable @{variable_ref ?case} refer to the
conclusion.
+ \<^descr> @{method "subproofs"}~\<open>m\<close> applies the method expression \<open>m\<close> consecutively
+ to each subgoal, constructing individual subproofs internally (analogous to
+ ``\<^theory_text>\<open>show goal by m\<close>'' for each subgoal of the proof state). Search
+ alternatives of \<open>m\<close> are truncated: the method is forced to be deterministic.
+ This method combinator impacts the internal construction of proof terms: it
+ makes a cascade of let-expressions within the derivation tree and may thus
+ improve scalability.
+
\<^descr> @{method "fact"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> composes some fact from \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> (or
implicitly from the current proof context) modulo unification of schematic
type and term variables. The rule structure is not taken into account, i.e.\