Skip to content
Success

Changes

Summary

  1. provide cache for slow computations;
  2. used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer
  3. more operations;
  4. more liberal parsing of Sledgehammer options to allow empty lists (as suggested by Larry Paulson)
Changeset 75068:99fcf3fda2fc by wenzelm:
provide cache for slow computations;
The file was modified src/Tools/Haskell/Haskell.thy (diff)
Changeset 75067:c23aa0d177b4 by desharna:
used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer
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)
Changeset 75066:fe81645c0b40 by wenzelm:
more operations;
The file was modified src/Tools/Haskell/Haskell.thy (diff)
Changeset 75065:7cadf5a7ed5b by blanchet:
more liberal parsing of Sledgehammer options to allow empty lists (as suggested by Larry Paulson)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML (diff)