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_tactics.ML
Mon, 25 Jul 2011 14:10:12 +0200 blanchet tuning file | diff | annotate
Thu, 14 Jul 2011 15:14:38 +0200 blanchet use monomorphic encoding as fallback, since they tend to produce fewer type errors 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
Sat, 25 Jun 2011 15:02:12 +0200 wenzelm produce string constant directly; file | diff | annotate
Thu, 09 Jun 2011 00:16:28 +0200 blanchet added a really fully typed translation as a fallback for Metis, in rare cases where Metis correctly proves a theorem but has type-unsound steps in it (which is likelier to happen with some of the lighter translations) file | diff | annotate
Thu, 09 Jun 2011 00:16:28 +0200 blanchet removed needless function that duplicated standard functionality, with a little unnecessary twist file | diff | annotate
Thu, 09 Jun 2011 00:16:28 +0200 blanchet be a bit more liberal with respect to the universal sort -- it sometimes help file | diff | annotate
Thu, 09 Jun 2011 00:16:28 +0200 blanchet renamed "untyped_aconv" to distinguish it clearly from the standard "aconv_untyped" file | diff | annotate
Tue, 07 Jun 2011 11:12:52 +0200 blanchet tuning file | diff | annotate
Tue, 07 Jun 2011 08:52:35 +0200 blanchet obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be file | diff | annotate
Mon, 06 Jun 2011 20:56:06 +0200 blanchet Metis code cleanup file | diff | annotate
Mon, 06 Jun 2011 20:36:36 +0200 blanchet enable new Metis file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet marked "metisF" as legacy -- nobody uses it or needs it file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet more preparations towards hijacking Metis file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet remove more occurrences of "metisX", preparing for the D Day when it will silently hijack "metis" and "metisFT" file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet make "metisX"'s default more like old "metis" file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet fixed type helper indices in new Metis file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet reveal Skolems in new Metis file | diff | annotate
Mon, 06 Jun 2011 20:36:34 +0200 blanchet use "metisX" as fallback, since it's much faster than "metisFT" 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 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes file | diff | annotate
Wed, 01 Jun 2011 10:29:43 +0200 blanchet more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done file | diff | annotate
Wed, 01 Jun 2011 10:29:43 +0200 blanchet make sure no warnings are given for polymorphic facts where we use a monomorphic instance file | diff | annotate
Wed, 01 Jun 2011 10:29:43 +0200 blanchet fixed Isabelle version of lightweight tag theorem, using "Thm.trivial" not "Thm.assume" 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
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 tuning 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 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 "metisX" syntax (temporary) 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
Mon, 30 May 2011 17:00:38 +0200 blanchet support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing file | diff | annotate
Fri, 27 May 2011 10:30:08 +0200 blanchet try both "metis" and (on failure) "metisFT" in replay file | diff | annotate
Thu, 19 May 2011 10:24:13 +0200 blanchet tuning file | diff | annotate
Thu, 12 May 2011 15:29:19 +0200 blanchet use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc. file | diff | annotate
Thu, 12 May 2011 15:29:19 +0200 blanchet added unfold set constant functionality to Meson/Metis -- disabled by default for now file | diff | annotate
Thu, 12 May 2011 15:29:19 +0200 blanchet more robust exception handling in Metis (also works if there are several subgoals) 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
Mon, 02 May 2011 16:33:21 +0200 wenzelm added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet added a hint to Metis errors suggesting metisFT -- it sometimes work 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:04 +0200 blanchet removed obsolete Skolem counter in new Skolemizer file | diff | annotate
Thu, 14 Apr 2011 11:24:04 +0200 blanchet improve definitional CNF on goal by moving "not" past the quantifiers file | diff | annotate
Tue, 23 Nov 2010 18:26:56 +0100 blanchet added "verbose" option to Metis to shut up its warnings if necessary file | diff | annotate
Fri, 29 Oct 2010 12:49:05 +0200 blanchet ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer) 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
Mon, 11 Oct 2010 18:03:18 +0700 blanchet added "trace_meson" configuration option, replacing old-fashioned reference file | diff | annotate
Mon, 11 Oct 2010 18:02:14 +0700 blanchet added "trace_metis" configuration option, replacing old-fashioned references file | diff | annotate
Wed, 06 Oct 2010 17:56:41 +0200 blanchet move code from "Metis_Tactics" to "Metis_Reconstruct" file | diff | annotate
Wed, 06 Oct 2010 17:42:57 +0200 blanchet get rid of function that duplicates existing Pure functionality file | diff | annotate
Wed, 06 Oct 2010 12:01:55 +0200 blanchet added a few FIXMEs file | diff | annotate
Tue, 05 Oct 2010 12:50:45 +0200 blanchet tuned comments file | diff | annotate
Tue, 05 Oct 2010 11:45:10 +0200 blanchet hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names file | diff | annotate
less more (0) -60 tip
isabelle