Changes

Summary

Changeset 78177:ea7a3cc64df5 by mathias fleury _mathias.fleury@mpi-inf.mpg.de_: early inclusion of cvc5 proof reconstruction; slightly reorganize smt/z3_reals;
The file was added	`src/HOL/Tools/SMT/cvc5_replay.ML`
The file was added	`src/HOL/Tools/SMT/cvc5_replay_methods.ML`
The file was modified	`CONTRIBUTORS` (diff)
The file was modified	`src/HOL/SMT.thy` (diff)
The file was modified	`src/HOL/SMT_Examples/Boogie_Dijkstra.certs` (diff)
The file was modified	`src/HOL/SMT_Examples/Boogie_Max.certs` (diff)
The file was modified	`src/HOL/SMT_Examples/SMT_Examples.certs` (diff)
The file was modified	`src/HOL/SMT_Examples/SMT_Examples_Verit.certs` (diff)
The file was modified	`src/HOL/SMT_Examples/SMT_Word_Examples.certs` (diff)
The file was modified	`src/HOL/SMT_Examples/VCC_Max.certs` (diff)
The file was modified	`src/HOL/Tools/SMT/cvc_proof_parse.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/lethe_proof.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/lethe_replay_methods.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/smt_config.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/smt_real.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/smt_replay_methods.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/smt_systems.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/smtlib_interface.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/verit_replay_methods.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/z3_real.ML` (diff)