Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. avoid error in Isar proof reconstruction if no ATP proof is available
  2. preplaying of 'smt' and 'metis' more in sync with actual method
  3. avoid generating polymorphic SPASS constructs to monomorphic SPASS
Changeset 62220:0e17a97234bd by blanchet:
avoid error in Isar proof reconstruction if no ATP proof is available
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML (diff)
Changeset 62219:dbac573b27e7 by blanchet:
preplaying of 'smt' and 'metis' more in sync with actual method
The file was modified src/HOL/Tools/Metis/metis_tactic.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML (diff)
Changeset 62218:42202671777c by blanchet:
avoid generating polymorphic SPASS constructs to monomorphic SPASS
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML (diff)