Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/atp_translate.ML
Thu, 19 Jan 2012 21:37:12 +0100 blanchet renamed "sound" option to "strict" file | diff | annotate
Tue, 03 Jan 2012 18:33:18 +0100 blanchet tuning file | diff | annotate
Mon, 02 Jan 2012 14:12:20 +0100 blanchet killed unfold_set_const option that makes no sense now that set is a type constructor again file | diff | annotate
Wed, 21 Dec 2011 15:04:28 +0100 blanchet killed "guard@?" encodings -- they were found to be unsound file | diff | annotate
Wed, 21 Dec 2011 15:04:28 +0100 blanchet extend previous optimizations to guard-based encodings file | diff | annotate
Wed, 21 Dec 2011 15:04:28 +0100 blanchet treat polymorphic constructors specially in @? encodings file | diff | annotate
Wed, 21 Dec 2011 15:04:28 +0100 blanchet tuning file | diff | annotate
Wed, 21 Dec 2011 15:04:28 +0100 blanchet no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil") file | diff | annotate
Tue, 20 Dec 2011 18:59:50 +0100 blanchet don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers file | diff | annotate
Tue, 20 Dec 2011 18:59:46 +0100 blanchet tuning file | diff | annotate
Tue, 20 Dec 2011 13:04:46 +0100 blanchet ensure TPTP FOF/TFF/THF formulas are close file | diff | annotate
Wed, 14 Dec 2011 18:07:32 +0100 blanchet make sure that all symbols are declared in untyped SPASS DFG output (broken since 3b8606fba2dd) file | diff | annotate
Tue, 13 Dec 2011 14:55:42 +0100 blanchet avoid multiple type decls in TFF (improves on cef82dc1462d) file | diff | annotate
Tue, 13 Dec 2011 14:55:42 +0100 blanchet added missing quantifier file | diff | annotate
Tue, 13 Dec 2011 14:55:42 +0100 blanchet remove needless declaration in TFF1 problems file | diff | annotate
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 file | diff | annotate
Wed, 07 Dec 2011 16:03:05 +0100 blanchet avoid multiple TFF1 declarations file | diff | annotate
Wed, 07 Dec 2011 16:03:05 +0100 blanchet updated TFF1 support file | diff | annotate
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 file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet 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 blanchet fixed bugs in lambda-lifting code -- ensure distinct names for variables file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet protect prefix against variant mutations file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet 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 blanchet removed needless baggage file | diff | annotate
Wed, 16 Nov 2011 16:35:19 +0100 blanchet thread in additional options to minimizer file | diff | annotate
Wed, 16 Nov 2011 13:22:36 +0100 blanchet make metis reconstruction handling more flexible file | diff | annotate
Wed, 16 Nov 2011 10:34:08 +0100 blanchet document "lam_trans" option file | diff | annotate
Wed, 16 Nov 2011 09:42:27 +0100 blanchet parse lambda translation option in Metis file | diff | annotate
Tue, 15 Nov 2011 22:20:58 +0100 blanchet rename the lambda translation schemes, so that they are understandable out of context file | diff | annotate
Tue, 15 Nov 2011 22:13:39 +0100 blanchet continued implementation of lambda-lifting in Metis file | diff | annotate
Tue, 15 Nov 2011 22:13:39 +0100 blanchet use consts, not frees, for lambda-lifting file | diff | annotate
Tue, 15 Nov 2011 22:13:39 +0100 blanchet started implementing lambda-lifting in Metis file | diff | annotate
Tue, 08 Nov 2011 08:56:23 +0100 blanchet made SML/NJ happy file | diff | annotate
Sun, 06 Nov 2011 22:18:54 +0100 blanchet tuning file | diff | annotate
Sun, 06 Nov 2011 11:13:47 +0100 blanchet repaired quantification over type variables for non-TFF1/THF encodings file | diff | annotate
Mon, 31 Oct 2011 17:51:01 +0100 blanchet improve handling of bound type variables (esp. for TFF1) file | diff | annotate
Mon, 31 Oct 2011 17:51:01 +0100 blanchet improved TFF1 output file | diff | annotate
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 file | diff | annotate
Sat, 29 Oct 2011 13:15:58 +0200 blanchet added DFG unsorted support (like in the old days) file | diff | annotate
Sat, 29 Oct 2011 13:15:58 +0200 blanchet added sorted DFG output for coming version of SPASS file | diff | annotate
Sat, 29 Oct 2011 13:15:58 +0200 blanchet check "sound" flag before doing something unsound... file | diff | annotate
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" file | diff | annotate
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 file | diff | annotate
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 file | diff | annotate
Sat, 10 Sep 2011 00:44:25 +0200 blanchet fixed definition of type intersection (soundness bug) file | diff | annotate
Fri, 09 Sep 2011 14:30:57 +0200 blanchet made SML/NJ happy file | diff | annotate
Thu, 08 Sep 2011 09:25:55 +0200 blanchet fixed computation of "in_conj" for polymorphic encodings file | diff | annotate
Wed, 07 Sep 2011 21:31:21 +0200 blanchet also implemented ghost version of the tagged encodings file | diff | annotate
Wed, 07 Sep 2011 21:31:21 +0200 blanchet smarter explicit apply business file | diff | annotate
Wed, 07 Sep 2011 21:31:21 +0200 blanchet started work on ghost type arg encoding file | diff | annotate
Wed, 07 Sep 2011 21:31:21 +0200 blanchet stricted type encoding parsing file | diff | annotate
Wed, 07 Sep 2011 13:50:17 +0200 blanchet tweaking polymorphic TFF and THF output file | diff | annotate
Wed, 07 Sep 2011 13:50:17 +0200 blanchet parse new experimental '@' encodings file | diff | annotate
Wed, 07 Sep 2011 13:50:17 +0200 blanchet tuning file | diff | annotate
Wed, 07 Sep 2011 13:50:16 +0200 blanchet tuning file | diff | annotate
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 file | diff | annotate
Wed, 07 Sep 2011 09:10:41 +0200 blanchet 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 blanchet tuning file | diff | annotate
Wed, 07 Sep 2011 09:10:41 +0200 blanchet make mangling sound w.r.t. type arguments file | diff | annotate
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 file | diff | annotate
less more (0) -100 -60 tip
isabelle