src/HOL/Tools/ATP/atp_problem_generate.ML
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
2012-07-10 blanchet 2012-07-10 tuning
2012-07-09 blanchet 2012-07-09 tuning
2012-07-05 blanchet 2012-07-05 make SML/NJ happy + tuning
2012-07-05 blanchet 2012-07-05 tune type arg handling
2012-07-05 blanchet 2012-07-05 tuning
2012-07-05 blanchet 2012-07-05 fiddled with "tags_at" a bit -- the only non-tuning part of the change is a slight simplification of the typing axioms
2012-07-05 blanchet 2012-07-05 remove needless type arguments to "tags_at" encoding
2012-07-04 blanchet 2012-07-04 more precise cover
2012-07-04 blanchet 2012-07-04 don't generate any type class axioms for free types for monomorphic encodings
2012-07-04 blanchet 2012-07-04 tuning
2012-06-26 blanchet 2012-06-26 reintroduced "t@" encoding, this time sound
2012-06-26 blanchet 2012-06-26 tuning
2012-06-26 blanchet 2012-06-26 renamed experimental option
2012-06-26 blanchet 2012-06-26 finished implementation of DFG type class output
2012-06-26 blanchet 2012-06-26 more work on DFG type classes
2012-06-26 blanchet 2012-06-26 more work on class support
2012-06-26 blanchet 2012-06-26 generate type classes for polymorphic DFG format (SPASS)
2012-06-26 blanchet 2012-06-26 avoid detour through terms
2012-06-26 blanchet 2012-06-26 cleanly distinguish between type declarations and symbol declarations
2012-06-26 blanchet 2012-06-26 removed old hack now that types and terms are cleanly distinguished in the data structure
2012-06-26 blanchet 2012-06-26 added sorts to datastructure
2012-06-26 blanchet 2012-06-26 robustness -- TFF1 does not support type classes
2012-06-26 blanchet 2012-06-26 implement polymorphic DFG output, without type classes for now
2012-06-26 blanchet 2012-06-26 added type arguments to "ATerm" constructor -- but don't use them yet
2012-06-26 blanchet 2012-06-26 started adding polymophic SPASS output
2012-06-26 blanchet 2012-06-26 tuning
2012-06-26 blanchet 2012-06-26 removed support for unsorted DFG, now that SPASS 3.7 is no longer supported
2012-06-18 blanchet 2012-06-18 sound monotonicity inference in the presence of "aggressive" helpers
2012-06-18 blanchet 2012-06-18 removed dead code
2012-06-06 blanchet 2012-06-06 prevent an "Empty" exception (e.g. with Satallax, "mono_native")
2012-06-06 blanchet 2012-06-06 tuning terminology
2012-06-06 blanchet 2012-06-06 added "args_query" encodings
2012-06-06 blanchet 2012-06-06 killed most unsound encodings
2012-06-06 blanchet 2012-06-06 generalized monotonic constructor optimisation so that it works with e.g. the product type
2012-06-06 blanchet 2012-06-06 removed micro-optimization whose justification I can't recall
2012-06-06 blanchet 2012-06-06 more aggressive type argument optimization
2012-06-06 blanchet 2012-06-06 use cover for "poly_guards" encoding
2012-06-06 blanchet 2012-06-06 hack to make LEO-II perform better on TPTP THF problems
2012-06-06 blanchet 2012-06-06 don't cripple Sledgehammer/ATP needlessly just because of "metis" -- there's also "smt" as a fallback anyway
2012-05-28 blanchet 2012-05-28 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
2012-05-28 blanchet 2012-05-28 don't generate definitions for LEO-II -- this cuases more harm than good
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-24 blanchet 2012-05-24 gracefully handle definition-looking premises
2012-05-23 blanchet 2012-05-23 order LEO-II/Satallax definitions so that they build on each other (cf. Satallax's THF policy)
2012-05-23 blanchet 2012-05-23 generate THF definitions
2012-05-23 wenzelm 2012-05-23 merged, abandoning change of src/HOL/Tools/ATP/atp_problem_generate.ML from 6ea205a4d7fd;
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-05-21 blanchet 2012-05-21 add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"