Summary
- fix veriT reconstruction for and_pos and lambda-lifting
- added lemmas image_mset_eq_{image_mset_plus,plus,plus_image_mset}D, and multp_image_mset_image_msetD
The file was modified | src/HOL/SMT_Examples/SMT_Tests_Verit.thy (diff) |
The file was modified | src/HOL/Tools/SMT/lethe_proof.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) |
The file was modified | NEWS (diff) |
The file was modified | src/HOL/Library/Multiset.thy (diff) |