Summary
- provide cache for slow computations;
- used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer
- more operations;
- more liberal parsing of Sledgehammer options to allow empty lists (as suggested by Larry Paulson)
The file was modified | src/Tools/Haskell/Haskell.thy (diff) |
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff) |
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML (diff) |
The file was modified | src/Tools/Haskell/Haskell.thy (diff) |
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML (diff) |