2012-01-19 blanchet 2012-01-19 renamed "sound" option to "strict"
2012-01-03 blanchet 2012-01-03 tuning
2012-01-02 blanchet 2012-01-02 killed unfold_set_const option that makes no sense now that set is a type constructor again
2011-12-21 blanchet 2011-12-21 killed "guard@?" encodings -- they were found to be unsound
2011-12-21 blanchet 2011-12-21 extend previous optimizations to guard-based encodings
2011-12-21 blanchet 2011-12-21 treat polymorphic constructors specially in @? encodings
2011-12-21 blanchet 2011-12-21 tuning
2011-12-21 blanchet 2011-12-21 no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")
2011-12-20 blanchet 2011-12-20 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
2011-12-20 blanchet 2011-12-20 tuning
2011-12-20 blanchet 2011-12-20 ensure TPTP FOF/TFF/THF formulas are close
2011-12-14 blanchet 2011-12-14 make sure that all symbols are declared in untyped SPASS DFG output (broken since 3b8606fba2dd)
2011-12-13 blanchet 2011-12-13 avoid multiple type decls in TFF (improves on cef82dc1462d)
2011-12-13 blanchet 2011-12-13 added missing quantifier
2011-12-13 blanchet 2011-12-13 remove needless declaration in TFF1 problems
2011-12-13 blanchet 2011-12-13 correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i
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