SMT reconstruction failures

[Makarius]

On 17/07/2025 22:22, Makarius wrote:
> 
> Doing a bisection, reveals the following result:
> 
> changeset:   82837:8aa1c98b948b
> user:        wenzelm
> date:        Fri Jul 11 14:03:09 2025 +0200
> files:       src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML src/Provers/ 
> classical.ML src/Pure/bires.ML
> description:
> maintain collective rule declarations via type Bires.decls, with netpair 
> operations derived from it;
> 
> 
> I've been there many times recently, to sort out remaining omissions in the 
> rather delicate treatment of classical rules.

I've finished this now, after a few more sidetracks:

changeset:   82890:72707b844734
user:        wenzelm
date:        Mon Jul 21 12:57:58 2025 +0200
files:       NEWS src/Pure/bires.ML
description:
clarified merge order: accurately reproduce the stable status-quo from 
53e56e6a67c3 --- e.g. relevant for smt proof reconstruction in (line 6705 of 
"$AFP/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy") of 
AFP/f1299d4f896c;

changeset:   15862:eae86974a665
tag:         tip
user:        wenzelm
date:        Mon Jul 21 15:24:31 2025 +0200
files:       thys/Buchi_Complementation/Complementation_Implement.thy 
thys/Tree_Enumeration/Rooted_Tree.thy
description:
backout d06954e7388a: no longer required thanks to Isabelle/72707b844734;


I will say more about the cumulative archeological findings on a different thread.


	Makarius