--- 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