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