Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)
Summary
- include unnamed chained facts in Sledgehammer's relevance filter
- merge
- removed hack in Sledgehammer that confuses preplay and gives Sledgehammer a strange semantics
- don't freeze terms in Sledgehammer, as this has a bad impact on 'using' facts
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML |
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML |
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML |
The file was modified | src/HOL/Tools/ATP/atp_problem_generate.ML |