Skip to content
Success

Changes

Summary

  1. fix veriT reconstruction for and_pos and lambda-lifting
  2. added lemmas image_mset_eq_{image_mset_plus,plus,plus_image_mset}D, and multp_image_mset_image_msetD
Changeset 75561:b6239ed66b94 by mathias fleury _mathias.fleury@mpi-inf.mpg.de_:
fix veriT reconstruction for and_pos and lambda-lifting
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)
Changeset 75560:aeb797356de0 by desharna:
added lemmas image_mset_eq_{image_mset_plus,plus,plus_image_mset}D, and multp_image_mset_image_msetD
The file was modified NEWS (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)