equal
deleted
inserted
replaced
49 the related option "proof_method" was removed. Proof reconstruction is |
49 the related option "proof_method" was removed. Proof reconstruction is |
50 supported directly by Sledgehammer and should be used instead. For |
50 supported directly by Sledgehammer and should be used instead. For |
51 more information, see Sledgehammer's documentation relating to |
51 more information, see Sledgehammer's documentation relating to |
52 "preplay_timeout". INCOMPATIBILITY. |
52 "preplay_timeout". INCOMPATIBILITY. |
53 - Added the action "order" testing the proof method of the same name. |
53 - Added the action "order" testing the proof method of the same name. |
|
54 |
|
55 * Session Data_Structures provides automatic translation from |
|
56 HOL functions into corresponding step-counting running-time functions.See theory Define_Time_Function. |
54 |
57 |
55 * Explicit type class for discrete_linear_ordered_semidom for integral |
58 * Explicit type class for discrete_linear_ordered_semidom for integral |
56 semidomains with a discrete linear order. |
59 semidomains with a discrete linear order. |
57 |
60 |
58 * Type class linordered_euclidean_semiring replaces the (rather |
61 * Type class linordered_euclidean_semiring replaces the (rather |