# HG changeset patch
# User wenzelm
# Date 1664559728 -7200
# Node ID 6ee5306d143ac9281b57bc93cffee7c433a86310
# Parent  3c46356d241f8f9f3eae073fd972cb362ad74858
more explanations on the new order prover (based on 10945fc183cd), without violating strict monotonicity of NEWS wrt. official releases;

diff -r 3c46356d241f -r 6ee5306d143a NEWS
--- a/NEWS	Fri Sep 30 19:26:28 2022 +0200
+++ b/NEWS	Fri Sep 30 19:42:08 2022 +0200
@@ -84,6 +84,51 @@
 by configuration option "record_sort_updates" (default: false). Some
 examples are in theory "HOL-Examples.Records".
 
+* More explanations on the new, verified order prover for partial and
+linear orders, which first appeared in Isabelle2021-1.
+
+The order prover rearranges the goal to prove False, then retrieves
+order literals (i.e. x = y, x <= y, x < y, and their negated versions)
+from the premises and finally tries to derive a contradiction. Its main
+use case is as a solver to the Simplifier, where it e.g. solves premises
+of conditional rewrite rules.
+
+The new prover (src/Provers/order_tac.ML) replaces the old prover
+(src/Provers/order.ML) and improves upon the old one in several ways:
+
+  - The completeness of the prover is verified in Isabelle (see the ATVA
+    2021 paper "A Verified Decision Procedure for Orders in
+    Isabelle/HOL").
+
+  - The new prover is complete for partial orders.
+
+  - The interface to register new orders was reworked to reduce
+    boilerplate.
+
+The prover has two configuration attributes that control its behaviour:
+
+  - order_trace (default: false) to enable tracing for the solver.
+
+  - order_split_limit (default: 8) to limit the number of order literals
+    of the form ~ x < y that are passed to the solver since those lead
+    to case splitting and thus exponential runtime. This only applies to
+    partial orders.
+
+The prover is agnostic to the object-logic, but the default setup is for
+HOL: see theory HOL.Orderings with ML structure HOL_Order_Tac. The
+structure allows us to register new orders with the functions
+HOL_Order_Tac.declare_order and HOL_Order_Tac.declare_linorder. Using
+these functions, we register the orders of the type classes order and
+linorder with the solver. If possible, one should instantiate these type
+classes instead of adding new orders to the solver. One can also
+interpret the type class locale as in src/HOL/Library/Sublist.thy, which
+contains e.g. the prefix order on lists.
+
+The proof method "order" invokes the prover in a standalone fashion.
+
+The diagnostic command 'print_orders' shows all orders known to the
+prover in the current context.
+
 * Meson: added support for polymorphic "using" facts. Minor
 INCOMPATIBILITY.