Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Metis/metis_reconstruct.ML
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 fixed recursive call in new path finder and (untested:) handle hAPP file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet more robust and simpler adjustment computation 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 first step in sharing more code between ATP and Metis translation 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: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
Sat, 16 Apr 2011 18:11:20 +0200 wenzelm eliminated old List.nth; 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 nicer error message from Metis for know failure that isn't the user's fault file | diff | annotate
Thu, 14 Apr 2011 11:24:05 +0200 blanchet make 48170228f562 work also with "HO_Reas" examples file | diff | annotate
Thu, 14 Apr 2011 11:24:05 +0200 blanchet improve on 0b05cc14c2cb: make sure that a literal variable "?foo" isn't accidentally renamed "?Q", which might be enough to confuse the new Skolemizer (cf. "Clausify.thy" example) file | diff | annotate
Thu, 14 Apr 2011 11:24:05 +0200 blanchet "unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now file | diff | annotate
Thu, 14 Apr 2011 11:24:05 +0200 blanchet handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377 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 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms file | diff | annotate
Thu, 14 Apr 2011 11:24:04 +0200 blanchet make new Skolemizer work also for "metisFT" file | diff | annotate
Thu, 14 Apr 2011 11:24:04 +0200 blanchet try to repair out-of-sync situations in Metis file | diff | annotate
Thu, 07 Apr 2011 12:16:27 +0200 blanchet further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind file | diff | annotate
Thu, 07 Apr 2011 12:16:26 +0200 blanchet make new Skolemizer more robust 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 remove newly added wrong logic file | diff | annotate
Thu, 24 Mar 2011 17:49:27 +0100 blanchet avoid evil "export_without_context", which breaks if there are local "fixes" 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:28 +0100 blanchet remove at most one double negation -- any other double negations are part of some higher-order reasoning and should be left alone, cf. "HO_Reas.thy" 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 tuning: unused var file | diff | annotate
Thu, 02 Dec 2010 14:56:16 +0100 blanchet give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def) file | diff | annotate
Fri, 26 Nov 2010 22:36:24 +0100 blanchet renamed "trace_me{son,tis}" and "verbose_metis" to have the name of the tool first 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 fixed order of quantifier instantiation in new Skolemizer file | diff | annotate
Fri, 29 Oct 2010 12:49:05 +0200 blanchet more work on new Skolemizer without Hilbert_Choice 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
Fri, 29 Oct 2010 12:49:05 +0200 blanchet make handling of parameters more robust, by querying the goal file | diff | annotate
Wed, 27 Oct 2010 16:32:13 +0200 blanchet do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p" file | diff | annotate
Tue, 26 Oct 2010 11:11:23 +0200 blanchet clearer error messages 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
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
Mon, 04 Oct 2010 22:45:09 +0200 blanchet move Metis into Plain file | diff | annotate | base
less more (0) tip
isabelle