src/Tools/auto_solve.ML
2009-11-24 wenzelm 2009-11-24 some rearangement of load order to keep preferences adjacent -- slightly fragile;
2009-10-29 wenzelm 2009-10-29 less hermetic ML; parse_pattern: apply Consts.intern only once (Why is this done anyway?); modernized structure names;
2009-10-28 wenzelm 2009-10-28 renamed Proof.flat_goal to Proof.simple_goal;
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
2009-10-02 wenzelm 2009-10-02 replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools; tuned;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-04-27 huffman 2009-04-27 merged
2009-04-25 wenzelm 2009-04-25 misc cleanup of auto_solve and quickcheck: tools are in src/Tools and loaded uniformly in HOL; preferences are configured in their proper place -- despite old misleading comments in the source; use predefined preferences categories; setmp preferences in-place;
2009-03-31 wenzelm 2009-03-31 fixed header; misc simplification, use Conjunction.dest_conjunctions;
2009-03-31 wenzelm 2009-03-31 superficial tuning;
2009-03-30 Timothy Bourke 2009-03-30 Limit the number of results returned by auto_solves.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-01 wenzelm 2009-03-01 replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already); minor tuning according to Isabelle coding conventions;
2009-02-27 wenzelm 2009-02-27 observe some Isabelle/ML coding conventions; avoid structure alias FT, which would complicate systematic searches unnecessarily;
2009-02-19 kleing 2009-02-19 half auto_solve default time out; increase manually in PG for large projects (L4v/Verisoft large).
2009-02-11 kleing 2009-02-11 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke