--- a/NEWS Thu Feb 29 16:55:10 2024 +0100
+++ b/NEWS Thu Feb 29 16:57:09 2024 +0100
@@ -23,32 +23,33 @@
+ Vampire 4.8 HO - Sledgehammer schedules (2023-10-19)
- New implementation of moura tactic. INCOMPATIBILITY.
-* Mirabelle:
- - Removed proof reconstruction from "sledgehammer" action; the related option
- "proof_method" was removed. Proof reconstruction is supported directly
- by Sledgehammer and should be used instead. For more information, see
- Sledgehammer's documentation relating to "preplay_timeout". INCOMPATIBILITY.
-
-* HOL-Analysis: the syntax of Lebesgue integrals (LINT, LBINT, \<integral>, etc.) now
- requires parentheses in most cases. INCOMPATIBILITY.
+* Mirabelle: Removed proof reconstruction from "sledgehammer" action;
+the related option "proof_method" was removed. Proof reconstruction is
+supported directly by Sledgehammer and should be used instead. For more
+information, see Sledgehammer's documentation relating to
+"preplay_timeout". INCOMPATIBILITY.
+
+* HOL-Analysis: the syntax of Lebesgue integrals (LINT, LBINT, \<integral>, etc.)
+now requires parentheses in most cases. INCOMPATIBILITY.
* HOL-Analysis: corrected the definition of convex function (convex_on)
- to require the underlying set to be convex. INCOMPATIBILITY.
+to require the underlying set to be convex. INCOMPATIBILITY.
* Explicit type class for discrete_linear_ordered_semidom for integral
- semidomains with a discrete linear order.
-
-* Type class linordered_euclidean_semiring replaces the (rather technical)
- type class unique_euclidean_semiring_with_nat; type class
- unique_euclidean_ring_with_nat, which barely admits instances other than
- isomorphic to int, is discontinued; type class
- unique_euclidean_semiring_with_bit_operations is renamed
- to linordered_euclidean_semiring_bit_operations. Minor INCOMPATIBILITY.
-
-* Streamlined specification of type class (semi)ring_parity. Minor
- INCOMPATIBILITY.
-
-* Lemma even_succ_div_2 renamed to even_half_succ_eq. Minor INCOMPATIBILITY.
+semidomains with a discrete linear order.
+
+* Type class linordered_euclidean_semiring replaces the (rather
+technical) type class unique_euclidean_semiring_with_nat; type class
+unique_euclidean_ring_with_nat, which barely admits instances other than
+isomorphic to int, is discontinued; type class
+unique_euclidean_semiring_with_bit_operations is renamed to
+linordered_euclidean_semiring_bit_operations. Minor INCOMPATIBILITY.
+
+* Streamlined specification of type class (semi)ring_parity. Minor
+INCOMPATIBILITY.
+
+* Lemma even_succ_div_2 renamed to even_half_succ_eq. Minor
+INCOMPATIBILITY.
* Theory "HOL.Transitive_Closure":
- Added lemmas.