[isabelle-dev] NEWS: A new, verified order prover.

[Makarius]

On 30/09/2022 12:51, Lukas Stevens wrote:
> *** HOL ***
> 
> * A new, verified order prover for partial and linear orders. 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.

Just for formal correctness and completeness of NEWS vs. repository vs. 
isabelle-dev mailing list, the relevant changesets are as follows:


changeset:   76226:2aad8698f82f
user:        Lukas Stevens <mail at lukas-stevens.de>
date:        Fri Sep 30 12:41:32 2022 +0200
files:       NEWS src/HOL/Orderings.thy
description:
tweaked

changeset:   76227:10945fc183cd
user:        Lukas Stevens <mail at lukas-stevens.de>
date:        Fri Sep 30 12:44:21 2022 +0200
files:       NEWS
description:
added documentation about new order prover

- new prover for partial and linear orders by Lukas Stevens and Tobias Nipkow

- See NEWS for more context

changeset:   76228:3c46356d241f
user:        wenzelm
date:        Fri Sep 30 19:26:28 2022 +0200
files:       NEWS
description:
restore NEWS, before commit accidents 2aad8698f82f and 10945fc183cd;

changeset:   76229:6ee5306d143a
tag:         tip
user:        wenzelm
date:        Fri Sep 30 19:42:08 2022 +0200
files:       NEWS
description:
more explanations on the new order prover (based on 10945fc183cd), without 
violating strict monotonicity of NEWS wrt. official releases;


As usual, I have tried my best to explain the purpose and intention of the 
change in the informal log, while making the formal diff as clear as possible. 
When studying the history, both the log and the diff together need to explain 
what was going in back in time.

The Isabelle Mercurial history serves like a formal proof of the final state 
of the sources. It needs to be written with great care, because it is ethernal 
and immutable --- nothing can be taken back without causing even greater harm.


We also have general explanations in README_REPOSITORY.

This is not the average Github project with incomprehensible history.


	Makarius