Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. post-merged into new Lethe code
  3. merged
  4. fixed generation of Isar proofs e89709b80b6e
  5. NEWS and CONTRIBUTORS
  6. nicer TPTP output
  7. regenerated
  8. tighter check to ensure that patterns remain left-linear, previous implementation was overcautious
  9. tuned
  10. tuned
Changeset 75368:b269a3c84b99 by desharna:
merged
Changeset 75367:1bad148d894f by desharna:
post-merged into new Lethe code
The file was modified src/HOL/Tools/SMT/lethe_proof_parse.ML (diff)
Changeset 75366:84c88a274ffd by desharna:
merged
Changeset 75365:83940294cc67 by desharna:
fixed generation of Isar proofs e89709b80b6e
The file was modified src/HOL/Tools/SMT/cvc4_proof_parse.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_translate.ML (diff)
The file was modified src/HOL/Tools/SMT/smtlib_interface.ML (diff)
The file was modified src/HOL/Tools/SMT/verit_proof_parse.ML (diff)
The file was modified src/HOL/Tools/SMT/verit_replay.ML (diff)
The file was modified src/HOL/Tools/SMT/z3_replay.ML (diff)
Changeset 75364:366f85a10407 by haftmann:
NEWS and CONTRIBUTORS
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
Changeset 75363:cf09060add1c by blanchet:
nicer TPTP output
The file was modified src/HOL/Tools/ATP/atp_problem.ML (diff)
Changeset 75362:4b8da5eef9d0 by haftmann:
regenerated
The file was modified src/HOL/Tools/Qelim/cooper_procedure.ML (diff)
Changeset 75361:f9c758208298 by haftmann:
tighter check to ensure that patterns remain left-linear, previous implementation was overcautious
The file was modified src/Tools/Code/code_thingol.ML (diff)
Changeset 75360:528768bc7bd0 by haftmann:
tuned
The file was modified src/Tools/Code/code_thingol.ML (diff)
Changeset 75359:1d08a01a7abb by haftmann:
tuned
The file was modified src/Tools/Code/code_thingol.ML (diff)