Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. removed redundant T_xxx_bound_aux lemmas
  3. don't generate not-fully-defined bit-vector constants in SMT problems
  4. improve and activate compression for veriT proof reconstruction
Changeset 72911:d02f91543bf1 by Peter Lammich:
merged
Changeset 72910:c145be662fbd by Peter Lammich:
removed redundant T_xxx_bound_aux lemmas
The file was modified src/HOL/Data_Structures/Binomial_Heap.thy (diff)
Changeset 72909:f9424ceea3c3 by mathias fleury _mathias.fleury@mpi-inf.mpg.de_:
don't generate not-fully-defined bit-vector constants in SMT problems
The file was modified src/HOL/Library/Tools/smt_word.ML (diff)
The file was modified src/HOL/SMT_Examples/SMT_Word_Examples.certs (diff)
Changeset 72908:6a26a955308e by mathias fleury _mathias.fleury@mpi-inf.mpg.de_:
improve and activate compression for veriT proof reconstruction
The file was modified src/HOL/SMT_Examples/SMT_Examples_Verit.thy (diff)
The file was modified src/HOL/Tools/SMT/smt_config.ML (diff)
The file was modified src/HOL/Tools/SMT/verit_proof.ML (diff)
The file was modified src/HOL/Tools/SMT/verit_replay_methods.ML (diff)