Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
  2. more lemmas
Changeset 72513:75f5c63f6cfa by mathias fleury _mathias.fleury@mpi-inf.mpg.de_:
better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
The file was modified src/HOL/SMT.thy (diff)
The file was modified src/HOL/SMT_Examples/SMT_Tests_Verit.thy (diff)
The file was modified src/HOL/Tools/SMT/smt_replay_arith.ML (diff)
The file was modified src/HOL/Tools/SMT/verit_proof.ML (diff)
The file was modified src/HOL/Tools/SMT/verit_replay.ML (diff)
The file was modified src/HOL/Tools/SMT/verit_replay_methods.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML (diff)
Changeset 72512:83b5911c0164 by haftmann:
more lemmas
The file was modified src/HOL/Int.thy (diff)
The file was modified src/HOL/Library/Bit_Operations.thy (diff)
The file was modified src/HOL/Numeral_Simprocs.thy (diff)
The file was modified src/HOL/Parity.thy (diff)
The file was modified src/HOL/Word/Word.thy (diff)