Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Metis/metis_translate.ML
Mon, 06 Jun 2011 20:36:35 +0200 blanchet tuning file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet conceal old Skolems in new Metis file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet properly locate helpers whose constants have several entries in the helper table file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet skip "hBOOL" in new Metis path finder file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet don't pass "~ " to new Metis file | diff | annotate
Mon, 06 Jun 2011 20:36:34 +0200 blanchet clean up unnecessary machinery -- helpers work also with monomorphic type encodings file | diff | annotate
Mon, 06 Jun 2011 20:36:34 +0200 blanchet added support for helpers in new Metis, so far only for polymorphic type encodings file | diff | annotate
Wed, 01 Jun 2011 10:29:43 +0200 blanchet ensured monomorphized facts have normalized zero var indexes, so that "find_var" doesn't fail later on file | diff | annotate
Wed, 01 Jun 2011 10:29:43 +0200 blanchet implemented missing hAPP and ti cases of new path finder file | diff | annotate
Wed, 01 Jun 2011 10:29:43 +0200 blanchet support lightweight tags in new Metis file | diff | annotate
Wed, 01 Jun 2011 10:29:43 +0200 blanchet tuned names file | diff | annotate
Wed, 01 Jun 2011 10:29:43 +0200 blanchet distinguish different kinds of typing informations in the fact name file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet monomorphize in the new Metis if the type system calls for it file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet fixed new path finder for type information tag file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet use ":" for type information (looks good in Metis's output) and handle it in new path finder file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet tuned name file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet tuned name file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet parse optional type system specification file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet proper handling of type variable classes in new Metis file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet don't preprocess twice file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet more work on new Metis file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet tuning file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet more work on new metis that exploits the powerful new type encodings file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet tuning file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet removed obscure option file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet added new metis mode, with no implementation yet file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet tuning file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet first step in sharing more code between ATP and Metis translation file | diff | annotate
Fri, 27 May 2011 10:30:07 +0200 blanchet tuning file | diff | annotate
Fri, 27 May 2011 10:30:07 +0200 blanchet cleaner handling of equality and proxies (esp. for THF) file | diff | annotate
Fri, 20 May 2011 18:01:46 +0200 blanchet name tuning file | diff | annotate
Fri, 20 May 2011 17:16:13 +0200 blanchet further improvements to "poly_{preds,tags}_{bang,query}" -- better solution to the combinator problem + make sure type assumptions can be discharged file | diff | annotate
Fri, 20 May 2011 17:16:13 +0200 blanchet prevent unsound combinator proofs in partially typed polymorphic type systems file | diff | annotate
Fri, 20 May 2011 12:47:58 +0200 blanchet tuning file | diff | annotate
Thu, 12 May 2011 15:29:19 +0200 blanchet handle equality proxy in a more backward-compatible way file | diff | annotate
Thu, 12 May 2011 15:29:19 +0200 blanchet reenabled equality proxy in Metis for higher-order reasoning file | diff | annotate
Thu, 12 May 2011 15:29:19 +0200 blanchet ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar) file | diff | annotate
Tue, 03 May 2011 14:23:40 +0200 blanchet reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis" file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet drop "fequal" type args for unmangled type systems file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0 file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet improve helper type instantiation code file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet killed needless datatype "combtyp" in Metis file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet have properly type-instantiated helper facts (combinators and If) file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet reimplemented the hAPP introduction code so that it's done earlier, when the types are still available file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet no point in keeping indices in Sledgehammer readable var names, since these are disambiguated anyway file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet added more rudimentary type support to Sledgehammer's ATP encoding file | diff | annotate
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context; file | diff | annotate
Thu, 14 Apr 2011 11:24:05 +0200 blanchet tuning file | diff | annotate
Thu, 24 Mar 2011 17:49:27 +0100 blanchet clean up new Skolemizer code -- some old hacks are no longer necessary file | diff | annotate
Thu, 24 Mar 2011 17:49:27 +0100 blanchet more robust handling of variables in new Skolemizer file | diff | annotate
Mon, 10 Jan 2011 15:45:46 +0100 wenzelm eliminated Int.toString; file | diff | annotate
Wed, 15 Dec 2010 11:26:29 +0100 blanchet tuning file | diff | annotate
Wed, 15 Dec 2010 11:26:28 +0100 blanchet added Sledgehammer support for higher-order propositional reasoning file | diff | annotate
Wed, 15 Dec 2010 11:26:28 +0100 blanchet add Metis support for higher-order propositional reasoning file | diff | annotate
Wed, 15 Dec 2010 11:26:28 +0100 blanchet implemented partially-typed "tags" type encoding file | diff | annotate
Fri, 29 Oct 2010 12:49:05 +0200 blanchet prevent type errors because of inconsistent skolem Var types by giving fresh indices to Skolems file | diff | annotate
Tue, 26 Oct 2010 11:10:00 +0200 blanchet renaming file | diff | annotate
Tue, 26 Oct 2010 10:57:04 +0200 blanchet no need to encode theorem number twice in skolem names file | diff | annotate
Wed, 06 Oct 2010 17:44:07 +0200 blanchet qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development) file | diff | annotate
Tue, 05 Oct 2010 12:50:45 +0200 blanchet tuned comments file | diff | annotate
less more (0) -60 tip
isabelle