src/HOL/Tools/ATP/atp_problem_generate.ML
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-01-31 blanchet 2014-01-31 tuning
2013-12-19 blanchet 2013-12-19 tuning
2013-12-19 blanchet 2013-12-19 tuning 'case' expressions
2013-12-19 blanchet 2013-12-19 extended ATP types with sorts
2013-12-18 blanchet 2013-12-18 generate type classes for tfrees
2013-12-17 blanchet 2013-12-17 tuning
2013-12-17 blanchet 2013-12-17 primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
2013-12-16 blanchet 2013-12-16 fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
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-11-14 blanchet 2013-11-14 implemented 'tptp_translate'
2013-10-24 blanchet 2013-10-24 use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations
2013-10-15 blanchet 2013-10-15 addressed rare case where the same symbol would be treated alternately as a function and as a predicate -- adding "top2I top_boolI" to a problem that didn't talk about "top" was a way to trigger the issue
2013-10-09 blanchet 2013-10-09 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
2013-09-12 blanchet 2013-09-12 prefixed types and some functions with "atp_" for disambiguation
2013-08-13 blanchet 2013-08-13 Vampire 3.0 requires types to be declared -- make it happy (and get rid of "implicit" types since only Satallax seems to support them anymore)
2013-05-24 blanchet 2013-05-24 improved handling of free variables' types in Isar proofs
2013-05-20 blanchet 2013-05-20 freeze types in Sledgehammer goal, not just terms
2013-05-19 blanchet 2013-05-19 made "completish" mode a bit more complete
2013-05-16 blanchet 2013-05-16 properly handle SPASS constructors w.r.t. partially applied functions
2013-05-16 blanchet 2013-05-16 tuned comments
2013-05-16 blanchet 2013-05-16 tuning
2013-05-16 blanchet 2013-05-16 more work on SPASS datatypes
2013-05-16 blanchet 2013-05-16 tuning -- renamed '_from_' to '_of_' in Sledgehammer
2013-05-16 blanchet 2013-05-16 compile
2013-05-16 blanchet 2013-05-16 don't recognize overloaded constants as constructors for the purpose of removing type arguments
2013-05-16 blanchet 2013-05-16 tuning
2013-05-16 blanchet 2013-05-16 reintroduced syntax for "nonexhaustive" datatypes
2013-05-16 blanchet 2013-05-16 tuning
2013-05-16 blanchet 2013-05-16 more work on SPASS datatypes
2013-05-15 blanchet 2013-05-15 tuning
2013-05-15 blanchet 2013-05-15 more work on SPASS datatypes
2013-05-15 blanchet 2013-05-15 more work on implementing datatype output for new SPASS
2013-05-15 blanchet 2013-05-15 renamed Sledgehammer functions with 'for' in their names to 'of'
2013-05-08 blanchet 2013-05-08 avoid polymorphic uncurried aliases with more arguments than there are arguments in the most general type of a HOL constant, to dodge issues at declaration time
2013-05-08 blanchet 2013-05-08 proper unmangling -- the bug is visible when "uncurried_aliases" is enabled with Alt-Ergo or Poly. SPASS
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-09 blanchet 2013-04-09 avoid duplicate "tcon_" names
2013-01-18 blanchet 2013-01-18 tuning
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
2013-01-07 blanchet 2013-01-07 tuned output
2013-01-03 blanchet 2013-01-03 close formulas in the natural order, not its reverse -- so that Skolem arguments appear in the right order in Isar proofs
2012-12-13 blanchet 2012-12-13 generate comments with original names for debugging
2012-10-31 blanchet 2012-10-31 tuned code
2012-09-12 wenzelm 2012-09-12 standardized ML aliases;
2012-08-02 blanchet 2012-08-02 don't tag negatively naked variables
2012-07-27 blanchet 2012-07-27 tweaks in preparation for type encoding evaluation
2012-07-27 blanchet 2012-07-27 bring implementation of traditional encoding in line with paper
2012-07-23 blanchet 2012-07-23 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
2012-07-18 blanchet 2012-07-18 speed up tautology/metaness check
2012-07-18 blanchet 2012-07-18 more consolidation of MaSh code
2012-07-18 blanchet 2012-07-18 more implementation work on MaSh
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 tuning