equal
deleted
inserted
replaced
22 * Mirabelle: |
22 * Mirabelle: |
23 - Removed proof reconstruction from "sledgehammer" action; the related option |
23 - Removed proof reconstruction from "sledgehammer" action; the related option |
24 "proof_method" was removed. Proof reconstruction is supported directly |
24 "proof_method" was removed. Proof reconstruction is supported directly |
25 by Sledgehammer and should be used instead. For more information, see |
25 by Sledgehammer and should be used instead. For more information, see |
26 Sledgehammer's documentation relating to "preplay_timeout". INCOMPATIBILITY. |
26 Sledgehammer's documentation relating to "preplay_timeout". INCOMPATIBILITY. |
|
27 |
|
28 * HOL-Analysis: corrected the definition of convex function (convex_on) |
|
29 to require the underlying set to be convex. INCOMPATIBILITY. |
27 |
30 |
28 * Explicit type class for discrete_linear_ordered_semidom for integral |
31 * Explicit type class for discrete_linear_ordered_semidom for integral |
29 semidomains with a discrete linear order. |
32 semidomains with a discrete linear order. |
30 |
33 |
31 * Type class linordered_euclidean_semiring replaces the (rather technical) |
34 * Type class linordered_euclidean_semiring replaces the (rather technical) |