src/HOL/Tools/ATP/atp_problem_generate.ML
2012-03-04 blanchet 2012-03-04 ensure no abstractions leak through after lambda-lifting (for formulas with higher-order occurrences of quantifiers)
2012-02-27 wenzelm 2012-02-27 more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
2012-02-24 blanchet 2012-02-24 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
2012-02-24 blanchet 2012-02-24 general solution to the arity bug that occasionally plagues Sledgehammer -- short story, lots of things go kaputt when a polymorphic symbol's arity in the translation is higher than the arity of the fully polymorphic HOL constant
2012-02-24 blanchet 2012-02-24 fixed arity bug with "If" helpers for "If" that returns a function
2012-02-10 blanchet 2012-02-10 be more gentle when generating KBO weights
2012-02-09 blanchet 2012-02-09 tune KBO weight code
2012-02-09 blanchet 2012-02-09 improved KBO weights -- beware of explicit applications
2012-02-09 blanchet 2012-02-09 added possibility of generating KBO weights to DFG problems
2012-02-06 blanchet 2012-02-06 fixed arity error
2012-02-06 blanchet 2012-02-06 renamed type encoding
2012-02-05 blanchet 2012-02-05 removed double filtering of type args
2012-02-04 blanchet 2012-02-04 made sure to filter type args also for "uncurried alias" equations
2012-02-04 blanchet 2012-02-04 made option available to users (mostly for experiments)
2012-02-03 blanchet 2012-02-03 extended SPASS/DFG output with ranks
2012-02-02 blanchet 2012-02-02 change 9ce354a77908 wasn't quite right -- here's an improvement
2012-02-02 blanchet 2012-02-02 don't introduce new symbols in helpers -- makes problems unprovable
2012-02-02 blanchet 2012-02-02 only constants can be aliased
2012-02-02 blanchet 2012-02-02 tuning
2012-02-02 blanchet 2012-02-02 implemented partial application aliases (for SPASS mainly)
2012-02-01 blanchet 2012-02-01 tuning
2012-01-31 blanchet 2012-01-31 third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
2012-01-31 blanchet 2012-01-31 improve SPASS setup
2012-01-31 blanchet 2012-01-31 new SPASS setup
2012-01-31 blanchet 2012-01-31 distinguish between ":lr" and ":lt" (terminating) in DFG format
2012-01-31 blanchet 2012-01-31 new try at lambda-lifting that works correctly for both Metis and Sledgehammer (cf. d724066ff3d0)
2012-01-31 blanchet 2012-01-31 reverted e2b1a86d59fc -- broke Metis's lambda-lifting
2012-01-30 blanchet 2012-01-30 fix debilitating bug with lambda lifting in conjectures with outer existential quantifiers
2012-01-30 blanchet 2012-01-30 new SPASS setup
2012-01-30 blanchet 2012-01-30 implemented new lambda translations scheme
2012-01-30 blanchet 2012-01-30 rename lambda translation schemes
2012-01-26 blanchet 2012-01-26 even more lr tags for SPASS -- anything that is considered an "equational rule spec" is relevant
2012-01-26 blanchet 2012-01-26 separate orthogonal components
2012-01-26 blanchet 2012-01-26 generate left-to-right rewrite tag for combinator helpers for SPASS 3.8
2012-01-26 blanchet 2012-01-26 better handling of individual type for DFG format (SPASS)
2012-01-23 blanchet 2012-01-23 renamed two files to make room for a new file