src/HOL/Tools/ATP/atp_util.ML
2017-06-06 wenzelm 2017-06-06 discontinued obsolete print mode;
2015-12-01 blanchet 2015-12-01 removed needless ML function
2015-12-01 blanchet 2015-12-01 tuned whitespace
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-01-24 wenzelm 2015-01-24 tuned signature;
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-11-06 wenzelm 2014-11-06 prefer explicit Keyword.keywords;
2014-08-28 blanchet 2014-08-28 reworked unskolemization for SPASS
2014-08-28 blanchet 2014-08-28 prefer '0.2 ms' to '249 \<mu>s'
2014-08-28 blanchet 2014-08-28 fixed second computations
2014-08-28 blanchet 2014-08-28 show microseconds as well (useful when playing with Isar proofs)
2014-08-01 blanchet 2014-08-01 remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer
2014-07-12 blanchet 2014-07-12 don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
2014-07-10 blanchet 2014-07-10 lambda-lifting for Z3 Isar proofs
2014-03-14 blanchet 2014-03-14 more simplification of trivial steps
2014-03-13 blanchet 2014-03-13 correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
2013-12-16 blanchet 2013-12-16 fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
2013-12-15 blanchet 2013-12-15 simplify generated propositions
2013-12-15 blanchet 2013-12-15 use 'prop' rather than 'bool' systematically in Isar reconstruction code
2013-11-21 blanchet 2013-11-21 eliminated Sledgehammer's dependency on old-style datatypes
2013-09-23 blanchet 2013-09-23 added "spy" option to Sledgehammer
2013-09-10 blanchet 2013-09-10 sorted out dependencies
2013-09-10 blanchet 2013-09-10 moved ML function closer to its remaining use
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-05-28 blanchet 2013-05-28 redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
2013-05-24 blanchet 2013-05-24 improved handling of free variables' types in Isar proofs
2013-05-20 blanchet 2013-05-20 parse agsyHOL proofs (as unsat cores)
2013-05-20 blanchet 2013-05-20 freeze types in Sledgehammer goal, not just terms
2013-05-16 blanchet 2013-05-16 tuning -- renamed '_from_' to '_of_' in Sledgehammer
2013-02-20 blanchet 2013-02-20 more simplifying constructors
2013-02-20 blanchet 2013-02-20 optimize Isar output some more
2013-01-18 blanchet 2013-01-18 pass correct index to "Sign.typ_unify" -- this is important to avoid what appears to be an infinite loop in the unifier
2012-11-26 wenzelm 2012-11-26 tuned signature; tuned;
2012-10-31 blanchet 2012-10-31 use metaquantification when possible in Isar proofs
2012-10-31 blanchet 2012-10-31 tuned code
2012-08-23 wenzelm 2012-08-23 prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
2012-08-11 blanchet 2012-08-11 fixed "double rev" bug that arose in situations where a % comment arose on the last line of a file without \n at the end
2012-07-18 blanchet 2012-07-18 optimized MaSh output by chunking it
2012-07-18 blanchet 2012-07-18 drastic overhaul of MaSh data structures + fixed a few performance issues
2012-07-11 blanchet 2012-07-11 moved most of MaSh exporter code to Sledgehammer
2012-07-11 blanchet 2012-07-11 optimized type intersection, hoping this will reduce the number of sudden Interrupts in the "incr_tvar" code
2012-07-10 blanchet 2012-07-10 tuning
2012-07-10 blanchet 2012-07-10 gracefully compute cardinality of sets (to avoid type protectors)
2012-05-24 blanchet 2012-05-24 make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)
2012-05-22 blanchet 2012-05-22 make higher-order goals more first-order via extensionality
2012-05-22 blanchet 2012-05-22 added "ext_cong_neq" lemma (not used yet); tuning
2012-04-24 blanchet 2012-04-24 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
2012-04-24 blanchet 2012-04-24 handle TPTP definitions as definitions in Nitpick rather than as axioms
2012-03-27 blanchet 2012-03-27 tuning (in particular, Symtab instead of AList)
2012-02-27 wenzelm 2012-02-27 more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
2012-01-31 blanchet 2012-01-31 third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
2011-12-16 wenzelm 2011-12-16 tuned signature;
2011-11-18 blanchet 2011-11-18 pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
2011-11-15 blanchet 2011-11-15 continued implementation of lambda-lifting in Metis
2011-10-29 blanchet 2011-10-29 check "sound" flag before doing something unsound...
2011-09-15 blanchet 2011-09-15 tail recursive proof preprocessing (needed for huge proofs)
2011-09-12 blanchet 2011-09-12 fixed type intersection (again)
2011-09-10 blanchet 2011-09-10 fixed definition of type intersection (soundness bug)