Summary
- avoid error in Isar proof reconstruction if no ATP proof is available
- preplaying of 'smt' and 'metis' more in sync with actual method
- avoid generating polymorphic SPASS constructs to monomorphic SPASS
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML (diff) |
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) |
The file was modified | src/HOL/Tools/ATP/atp_problem_generate.ML (diff) |