NEWS
changeset 80034 95b4fb2b5359
parent 80020 b0a46cf73aa4
child 80041 a0f93621c332
--- a/NEWS	Wed Mar 27 10:54:47 2024 +0100
+++ b/NEWS	Wed Mar 27 15:16:09 2024 +0000
@@ -61,6 +61,9 @@
     "preplay_timeout". INCOMPATIBILITY.
   - Added the action "order" testing the proof method of the same name.
 
+* HOL-ex.Sketch_and_Explore: improvements to generate more natural and
+readable proof sketches from proof states.
+
 * Explicit type class for discrete_linear_ordered_semidom for integral
 semidomains with a discrete linear order.