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
Tue, 23 Aug 2011 14:44:19 +0200 blanchet fixed TFF slicing file | diff | annotate
Tue, 23 Aug 2011 14:44:19 +0200 blanchet added formats to the slice and use TFF for remote Vampire file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet we must tag any type whose ground types intersect a nonmonotonic type file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet made reconstruction of type tag equalities "\?x = \?x" reliable file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet revert guard logic -- make sure that typing information is generated for existentials file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet generate tag equations for existential variables file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet tuning, plus started implementing tag equation generation for existential variables file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet clearer terminology file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet added caching for (in)finiteness checks file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet remove needless typing information file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet cleaner handling of polymorphic monotonicity inference file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet added option to control soundness of encodings more precisely, for evaluation purposes file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet make sound mode more sound (and clean up code) file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false file | diff | annotate
Wed, 17 Aug 2011 10:03:58 +0200 blanchet distinguish THF syntax with and without choice (Satallax vs. LEO-II) file | diff | annotate
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy; file | diff | annotate
Tue, 09 Aug 2011 17:33:17 +0200 blanchet workaround THF parser limitation file | diff | annotate
Tue, 09 Aug 2011 09:05:22 +0200 blanchet move lambda-lifting code to ATP encoding, so it can be used by Metis file | diff | annotate
Thu, 28 Jul 2011 16:32:49 +0200 blanchet added helpers for "All" and "Ex" file | diff | annotate
Thu, 28 Jul 2011 16:32:39 +0200 blanchet no needless mangling file | diff | annotate
Thu, 28 Jul 2011 11:43:45 +0200 blanchet fixed lambda concealing file | diff | annotate
Tue, 26 Jul 2011 22:53:06 +0200 blanchet renamed "preds" encodings to "guards" file | diff | annotate
Tue, 26 Jul 2011 14:53:00 +0200 blanchet further worked around LEO-II parser limitation, with eta-expansion file | diff | annotate
Tue, 26 Jul 2011 14:53:00 +0200 blanchet no need for existential witnesses for sorts in TFF and THF formats file | diff | annotate
Tue, 26 Jul 2011 14:53:00 +0200 blanchet mangle "undefined" file | diff | annotate
Mon, 25 Jul 2011 14:10:12 +0200 blanchet declare "undefined" constant file | diff | annotate
Mon, 25 Jul 2011 14:10:12 +0200 blanchet avoid needless type args for lifted-lambdas file | diff | annotate
Thu, 21 Jul 2011 21:29:10 +0200 blanchet make "concealed" lambda translation sound file | diff | annotate
Wed, 20 Jul 2011 23:47:27 +0200 blanchet use a more robust naming convention for "polymorphic" frees -- the check is an overapproximation but that's fine as far as soundness is concerned file | diff | annotate
Wed, 20 Jul 2011 00:37:42 +0200 blanchet pass type arguments to lambda-lifted Frees, to account for polymorphism file | diff | annotate
Wed, 20 Jul 2011 00:37:42 +0200 blanchet generate slightly less type information -- this should be sound since type arguments should keep things cleanly apart file | diff | annotate
Wed, 20 Jul 2011 00:37:42 +0200 blanchet avoid calling "Term.is_first_order" (indirectly) on a term with loose de Bruijns -- this is not necessary anyway because of the Abs check in "simple_translate_lambdas" file | diff | annotate
Sun, 17 Jul 2011 14:21:19 +0200 blanchet fixed lambda-liftg: must ensure the formulas are in close form file | diff | annotate
Sun, 17 Jul 2011 14:12:45 +0200 blanchet ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names) file | diff | annotate
Sun, 17 Jul 2011 14:11:35 +0200 blanchet pass kind to lambda-translation function file | diff | annotate
Sun, 17 Jul 2011 14:11:35 +0200 blanchet more refactoring of preprocessing file | diff | annotate
Sun, 17 Jul 2011 14:11:35 +0200 blanchet more refactoring of preprocessing, so as to be able to centralize it file | diff | annotate
Sun, 17 Jul 2011 14:11:35 +0200 blanchet renamed internal data structure file | diff | annotate
Sun, 17 Jul 2011 14:11:35 +0200 blanchet simplify code -- there are no lambdas in helpers anyway file | diff | annotate
Sun, 17 Jul 2011 14:11:35 +0200 blanchet added lambda-lifting to Sledgehammer (rough) file | diff | annotate
Sun, 17 Jul 2011 14:11:34 +0200 blanchet move more lambda-handling logic to Sledgehammer, from ATP module, for formal dependency reasons file | diff | annotate
Thu, 14 Jul 2011 17:29:30 +0200 blanchet move error logic closer to user file | diff | annotate
Thu, 14 Jul 2011 16:50:05 +0200 blanchet move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators) file | diff | annotate
Thu, 14 Jul 2011 16:50:05 +0200 blanchet added option to control which lambda translation to use (for experiments) file | diff | annotate
Wed, 06 Jul 2011 17:19:34 +0100 blanchet make SML/NJ happier file | diff | annotate
Wed, 06 Jul 2011 17:19:34 +0100 blanchet make SML/NJ happy + tuning file | diff | annotate
Tue, 05 Jul 2011 17:09:59 +0100 nik improved translation of lambdas in THF file | diff | annotate
Tue, 05 Jul 2011 17:09:59 +0100 nik added generation of lambdas in THF file | diff | annotate
Tue, 05 Jul 2011 17:09:59 +0100 nik add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order) file | diff | annotate
Fri, 01 Jul 2011 15:53:38 +0200 blanchet further repair "mangled_tags", now that tags are also mangled file | diff | annotate
Fri, 01 Jul 2011 15:53:38 +0200 blanchet renamed "type_sys" to "type_enc", which is more accurate file | diff | annotate
Fri, 01 Jul 2011 15:53:37 +0200 blanchet cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company file | diff | annotate
Fri, 01 Jul 2011 15:53:37 +0200 blanchet mangle "ti" tags file | diff | annotate
Fri, 01 Jul 2011 15:53:37 +0200 blanchet tuning file | diff | annotate
Mon, 27 Jun 2011 14:56:28 +0200 blanchet added "sound" option to force Sledgehammer to be pedantically sound file | diff | annotate
Tue, 21 Jun 2011 17:17:39 +0200 blanchet don't change the way helpers are generated for the exporter's sake file | diff | annotate
Tue, 21 Jun 2011 17:17:39 +0200 blanchet remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations file | diff | annotate
Tue, 21 Jun 2011 17:17:39 +0200 blanchet avoid double ASCII-fication file | diff | annotate
less more (0) -100 -60 tip
isabelle