# HG changeset patch
# User wenzelm
# Date 1565720163 -7200
# Node ID f2d58cafbc13309fd84eb9812035cfdb02141006
# Parent  9ddd66d53130ba12fbca711d05a69595dcd25c0a
more documentation;

diff -r 9ddd66d53130 -r f2d58cafbc13 NEWS
--- 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
diff -r 9ddd66d53130 -r f2d58cafbc13 src/Doc/Isar_Ref/Proof.thy
--- 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.\