src/HOL/Tools/ATP/atp_translate.ML
Tue, 13 Dec 2011 14:55:42 +0100 blanchet added missing quantifier
Tue, 13 Dec 2011 14:55:42 +0100 blanchet remove needless declaration in TFF1 problems
Tue, 13 Dec 2011 14:55:42 +0100 blanchet correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i
Wed, 07 Dec 2011 16:03:05 +0100 blanchet avoid multiple TFF1 declarations
Wed, 07 Dec 2011 16:03:05 +0100 blanchet updated TFF1 support
Fri, 18 Nov 2011 11:47:12 +0100 blanchet pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
Fri, 18 Nov 2011 11:47:12 +0100 blanchet move eta-contraction to before translation to Metis, to ensure everything stays in sync
Fri, 18 Nov 2011 11:47:12 +0100 blanchet fixed bugs in lambda-lifting code -- ensure distinct names for variables
Fri, 18 Nov 2011 11:47:12 +0100 blanchet protect prefix against variant mutations
Fri, 18 Nov 2011 11:47:12 +0100 blanchet don't pass "lam_lifted" option to "metis" unless there's a good reason
Fri, 18 Nov 2011 11:47:12 +0100 blanchet removed needless baggage
Wed, 16 Nov 2011 16:35:19 +0100 blanchet thread in additional options to minimizer
Wed, 16 Nov 2011 13:22:36 +0100 blanchet make metis reconstruction handling more flexible
Wed, 16 Nov 2011 10:34:08 +0100 blanchet document "lam_trans" option
Wed, 16 Nov 2011 09:42:27 +0100 blanchet parse lambda translation option in Metis
Tue, 15 Nov 2011 22:20:58 +0100 blanchet rename the lambda translation schemes, so that they are understandable out of context
Tue, 15 Nov 2011 22:13:39 +0100 blanchet continued implementation of lambda-lifting in Metis
Tue, 15 Nov 2011 22:13:39 +0100 blanchet use consts, not frees, for lambda-lifting
Tue, 15 Nov 2011 22:13:39 +0100 blanchet started implementing lambda-lifting in Metis
Tue, 08 Nov 2011 08:56:23 +0100 blanchet made SML/NJ happy
Sun, 06 Nov 2011 22:18:54 +0100 blanchet tuning
Sun, 06 Nov 2011 11:13:47 +0100 blanchet repaired quantification over type variables for non-TFF1/THF encodings
Mon, 31 Oct 2011 17:51:01 +0100 blanchet improve handling of bound type variables (esp. for TFF1)
Mon, 31 Oct 2011 17:51:01 +0100 blanchet improved TFF1 output
Sat, 29 Oct 2011 13:15:58 +0200 blanchet 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
Sat, 29 Oct 2011 13:15:58 +0200 blanchet added DFG unsorted support (like in the old days)
Sat, 29 Oct 2011 13:15:58 +0200 blanchet added sorted DFG output for coming version of SPASS
Sat, 29 Oct 2011 13:15:58 +0200 blanchet check "sound" flag before doing something unsound...
Wed, 19 Oct 2011 16:36:13 +0200 blanchet avoid generating too meta theorems -- this sometimes leads to type errors, e.g. when "pp" is applied to a "prop" instead of a "bool"
Tue, 18 Oct 2011 15:40:59 +0200 blanchet freeze conjecture schematics before applying lambda-translation, which sometimes calls "close_form" and ruins it for freezing
Tue, 18 Oct 2011 15:40:58 +0200 blanchet gracefully handle quantifiers of the form "All $ t" where "t" is not a lambda-abstraction in higher-order translations
Sat, 10 Sep 2011 00:44:25 +0200 blanchet fixed definition of type intersection (soundness bug)
Fri, 09 Sep 2011 14:30:57 +0200 blanchet made SML/NJ happy
Thu, 08 Sep 2011 09:25:55 +0200 blanchet fixed computation of "in_conj" for polymorphic encodings
Wed, 07 Sep 2011 21:31:21 +0200 blanchet also implemented ghost version of the tagged encodings
Wed, 07 Sep 2011 21:31:21 +0200 blanchet smarter explicit apply business
Wed, 07 Sep 2011 21:31:21 +0200 blanchet started work on ghost type arg encoding
Wed, 07 Sep 2011 21:31:21 +0200 blanchet stricted type encoding parsing
Wed, 07 Sep 2011 13:50:17 +0200 blanchet tweaking polymorphic TFF and THF output
Wed, 07 Sep 2011 13:50:17 +0200 blanchet parse new experimental '@' encodings
Wed, 07 Sep 2011 13:50:17 +0200 blanchet tuning
Wed, 07 Sep 2011 13:50:16 +0200 blanchet tuning
Wed, 07 Sep 2011 09:10:41 +0200 blanchet 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
Wed, 07 Sep 2011 09:10:41 +0200 blanchet perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
Wed, 07 Sep 2011 09:10:41 +0200 blanchet tuning
Wed, 07 Sep 2011 09:10:41 +0200 blanchet make mangling sound w.r.t. type arguments
Wed, 07 Sep 2011 09:10:41 +0200 blanchet make "filter_type_args" more robust if the actual arity is higher than the declared one
Wed, 07 Sep 2011 09:10:41 +0200 blanchet rationalize uniform encodings
Tue, 06 Sep 2011 18:13:36 +0200 blanchet added dummy polymorphic THF system
Tue, 06 Sep 2011 11:31:01 +0200 blanchet cleanup "simple" type encodings
Tue, 06 Sep 2011 09:11:08 +0200 blanchet drop more type arguments soundly, when they can be deduced from the arg types
Thu, 01 Sep 2011 13:18:27 +0200 blanchet make "sound" sound and "unsound" more sound, based on evaluation
Wed, 31 Aug 2011 13:22:50 +0200 blanchet make SML/NJ happy
Wed, 31 Aug 2011 11:52:03 +0200 blanchet more tuning
Wed, 31 Aug 2011 11:23:16 +0200 blanchet more tuning
Wed, 31 Aug 2011 11:14:53 +0200 blanchet tuning
Wed, 31 Aug 2011 11:12:27 +0200 blanchet avoid relying on dubious TFF1 feature
Tue, 30 Aug 2011 16:07:46 +0200 blanchet generate properly typed TFF1 (PFF) problems in the presence of type class predicates
Tue, 30 Aug 2011 16:07:45 +0200 blanchet added type abstractions (for declaring polymorphic constants) to TFF syntax
Tue, 30 Aug 2011 16:07:45 +0200 blanchet implement more of the polymorphic simply typed format TFF(1)
less more (0) -100 -60 tip