equal
deleted
inserted
replaced
58 option "proof_method" was removed. Proof reconstruction is supported |
58 option "proof_method" was removed. Proof reconstruction is supported |
59 directly by Sledgehammer and should be used instead. For more |
59 directly by Sledgehammer and should be used instead. For more |
60 information, see Sledgehammer's documentation relating to |
60 information, see Sledgehammer's documentation relating to |
61 "preplay_timeout". INCOMPATIBILITY. |
61 "preplay_timeout". INCOMPATIBILITY. |
62 - Added the action "order" testing the proof method of the same name. |
62 - Added the action "order" testing the proof method of the same name. |
|
63 |
|
64 * HOL-ex.Sketch_and_Explore: improvements to generate more natural and |
|
65 readable proof sketches from proof states. |
63 |
66 |
64 * Explicit type class for discrete_linear_ordered_semidom for integral |
67 * Explicit type class for discrete_linear_ordered_semidom for integral |
65 semidomains with a discrete linear order. |
68 semidomains with a discrete linear order. |
66 |
69 |
67 * Type class linordered_euclidean_semiring replaces the (rather |
70 * Type class linordered_euclidean_semiring replaces the (rather |