src/HOL/Tools/ATP/atp_translate.ML
2011-12-07 blanchet 2011-12-07 avoid multiple TFF1 declarations
2011-12-07 blanchet 2011-12-07 updated TFF1 support
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-18 blanchet 2011-11-18 move eta-contraction to before translation to Metis, to ensure everything stays in sync
2011-11-18 blanchet 2011-11-18 fixed bugs in lambda-lifting code -- ensure distinct names for variables
2011-11-18 blanchet 2011-11-18 protect prefix against variant mutations
2011-11-18 blanchet 2011-11-18 don't pass "lam_lifted" option to "metis" unless there's a good reason
2011-11-18 blanchet 2011-11-18 removed needless baggage
2011-11-16 blanchet 2011-11-16 thread in additional options to minimizer
2011-11-16 blanchet 2011-11-16 make metis reconstruction handling more flexible
2011-11-16 blanchet 2011-11-16 document "lam_trans" option
2011-11-16 blanchet 2011-11-16 parse lambda translation option in Metis
2011-11-15 blanchet 2011-11-15 rename the lambda translation schemes, so that they are understandable out of context
2011-11-15 blanchet 2011-11-15 continued implementation of lambda-lifting in Metis
2011-11-15 blanchet 2011-11-15 use consts, not frees, for lambda-lifting
2011-11-15 blanchet 2011-11-15 started implementing lambda-lifting in Metis
2011-11-08 blanchet 2011-11-08 made SML/NJ happy
2011-11-06 blanchet 2011-11-06 tuning
2011-11-06 blanchet 2011-11-06 repaired quantification over type variables for non-TFF1/THF encodings
2011-10-31 blanchet 2011-10-31 improve handling of bound type variables (esp. for TFF1)
2011-10-31 blanchet 2011-10-31 improved TFF1 output
2011-10-29 blanchet 2011-10-29 always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions
2011-10-29 blanchet 2011-10-29 added DFG unsorted support (like in the old days)
2011-10-29 blanchet 2011-10-29 added sorted DFG output for coming version of SPASS
2011-10-29 blanchet 2011-10-29 check "sound" flag before doing something unsound...
2011-10-19 blanchet 2011-10-19 avoid generating too meta theorems -- this sometimes leads to type errors, e.g. when "pp" is applied to a "prop" instead of a "bool"
2011-10-18 blanchet 2011-10-18 freeze conjecture schematics before applying lambda-translation, which sometimes calls "close_form" and ruins it for freezing
2011-10-18 blanchet 2011-10-18 gracefully handle quantifiers of the form "All $ t" where "t" is not a lambda-abstraction in higher-order translations
2011-09-10 blanchet 2011-09-10 fixed definition of type intersection (soundness bug)
2011-09-09 blanchet 2011-09-09 made SML/NJ happy
2011-09-08 blanchet 2011-09-08 fixed computation of "in_conj" for polymorphic encodings
2011-09-07 blanchet 2011-09-07 also implemented ghost version of the tagged encodings
2011-09-07 blanchet 2011-09-07 smarter explicit apply business
2011-09-07 blanchet 2011-09-07 started work on ghost type arg encoding
2011-09-07 blanchet 2011-09-07 stricted type encoding parsing
2011-09-07 blanchet 2011-09-07 tweaking polymorphic TFF and THF output
2011-09-07 blanchet 2011-09-07 parse new experimental '@' encodings
2011-09-07 blanchet 2011-09-07 tuning
2011-09-07 blanchet 2011-09-07 tuning
2011-09-07 blanchet 2011-09-07 separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
2011-09-07 blanchet 2011-09-07 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
2011-09-07 blanchet 2011-09-07 tuning
2011-09-07 blanchet 2011-09-07 make mangling sound w.r.t. type arguments
2011-09-07 blanchet 2011-09-07 make "filter_type_args" more robust if the actual arity is higher than the declared one
2011-09-07 blanchet 2011-09-07 rationalize uniform encodings
2011-09-06 blanchet 2011-09-06 added dummy polymorphic THF system
2011-09-06 blanchet 2011-09-06 cleanup "simple" type encodings
2011-09-06 blanchet 2011-09-06 drop more type arguments soundly, when they can be deduced from the arg types
2011-09-01 blanchet 2011-09-01 make "sound" sound and "unsound" more sound, based on evaluation
2011-08-31 blanchet 2011-08-31 make SML/NJ happy
2011-08-31 blanchet 2011-08-31 more tuning
2011-08-31 blanchet 2011-08-31 more tuning
2011-08-31 blanchet 2011-08-31 tuning
2011-08-31 blanchet 2011-08-31 avoid relying on dubious TFF1 feature
2011-08-30 blanchet 2011-08-30 generate properly typed TFF1 (PFF) problems in the presence of type class predicates
2011-08-30 blanchet 2011-08-30 added type abstractions (for declaring polymorphic constants) to TFF syntax
2011-08-30 blanchet 2011-08-30 implement more of the polymorphic simply typed format TFF(1)
2011-08-30 blanchet 2011-08-30 extended simple types with polymorphism -- the implementation still needs some work though
2011-08-30 blanchet 2011-08-30 first step towards polymorphic TFF + changed defaults for Vampire
2011-08-30 nik 2011-08-30 removed explicit reliance on Hilbert_Choice.Eps