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.