Summary
- merged
- removed redundant T_xxx_bound_aux lemmas
- don't generate not-fully-defined bit-vector constants in SMT problems
- improve and activate compression for veriT proof reconstruction
The file was modified | src/HOL/Data_Structures/Binomial_Heap.thy (diff) |
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) |
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) |