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: the syntax of Lebesgue integrals (LINT, LBINT, \<integral>, etc.) now |
|
29 requires parentheses in most cases. INCOMPATIBILITY. |
27 |
30 |
28 * HOL-Analysis: corrected the definition of convex function (convex_on) |
31 * HOL-Analysis: corrected the definition of convex function (convex_on) |
29 to require the underlying set to be convex. INCOMPATIBILITY. |
32 to require the underlying set to be convex. INCOMPATIBILITY. |
30 |
33 |
31 * Explicit type class for discrete_linear_ordered_semidom for integral |
34 * Explicit type class for discrete_linear_ordered_semidom for integral |