src/HOL/Tools/Metis/metis_reconstruct.ML
Wed, 08 Jun 2011 16:20:18 +0200 blanchet restore comment about subtle issue
Wed, 08 Jun 2011 15:56:57 +0200 wenzelm more robust exception pattern General.Subscript;
Wed, 08 Jun 2011 08:47:43 +0200 blanchet removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
Wed, 08 Jun 2011 08:47:43 +0200 blanchet removed experimental code submitted by mistake
Wed, 08 Jun 2011 08:47:43 +0200 blanchet killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
Tue, 07 Jun 2011 10:43:18 +0200 blanchet nicely thread monomorphism verbosity in Metis and Sledgehammer
Mon, 06 Jun 2011 20:56:06 +0200 blanchet Metis code cleanup
Mon, 06 Jun 2011 20:36:35 +0200 blanchet fall back in case path finder fails -- these errors are sometimes salvageable
Mon, 06 Jun 2011 20:36:35 +0200 blanchet more preparations towards hijacking Metis
Mon, 06 Jun 2011 20:36:35 +0200 blanchet improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
Mon, 06 Jun 2011 20:36:35 +0200 blanchet make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
Mon, 06 Jun 2011 20:36:35 +0200 blanchet tuning
Mon, 06 Jun 2011 20:36:35 +0200 blanchet reveal Skolems in new Metis
Mon, 06 Jun 2011 20:36:35 +0200 blanchet properly unmangle names in path finder
Mon, 06 Jun 2011 20:36:35 +0200 blanchet skip "hBOOL" in new Metis path finder
Mon, 06 Jun 2011 20:36:34 +0200 blanchet added Metis examples to test the new type encodings
Mon, 06 Jun 2011 20:36:34 +0200 blanchet added support for helpers in new Metis, so far only for polymorphic type encodings
Wed, 01 Jun 2011 10:29:43 +0200 blanchet handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
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
Wed, 01 Jun 2011 10:29:43 +0200 blanchet make sure no warnings are given for polymorphic facts where we use a monomorphic instance
Wed, 01 Jun 2011 10:29:43 +0200 blanchet implemented missing hAPP and ti cases of new path finder
Wed, 01 Jun 2011 10:29:43 +0200 blanchet tuned names
Tue, 31 May 2011 16:38:36 +0200 blanchet fixed new path finder for type information tag
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
Tue, 31 May 2011 16:38:36 +0200 blanchet tuned name
Tue, 31 May 2011 16:38:36 +0200 blanchet fixed recursive call in new path finder and (untested:) handle hAPP
Tue, 31 May 2011 16:38:36 +0200 blanchet more robust and simpler adjustment computation
Tue, 31 May 2011 16:38:36 +0200 blanchet more work on new Metis
Tue, 31 May 2011 16:38:36 +0200 blanchet tuning
Tue, 31 May 2011 16:38:36 +0200 blanchet more work on new metis that exploits the powerful new type encodings
Tue, 31 May 2011 16:38:36 +0200 blanchet first step in sharing more code between ATP and Metis translation
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"
Mon, 02 May 2011 16:33:21 +0200 wenzelm added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
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
Sat, 16 Apr 2011 18:11:20 +0200 wenzelm eliminated old List.nth;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Thu, 14 Apr 2011 11:24:05 +0200 blanchet nicer error message from Metis for know failure that isn't the user's fault
Thu, 14 Apr 2011 11:24:05 +0200 blanchet make 48170228f562 work also with "HO_Reas" examples
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)
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
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
Thu, 14 Apr 2011 11:24:04 +0200 blanchet removed obsolete Skolem counter in new Skolemizer
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
Thu, 14 Apr 2011 11:24:04 +0200 blanchet make new Skolemizer work also for "metisFT"
Thu, 14 Apr 2011 11:24:04 +0200 blanchet try to repair out-of-sync situations in Metis
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
Thu, 07 Apr 2011 12:16:26 +0200 blanchet make new Skolemizer more robust
Thu, 24 Mar 2011 17:49:27 +0100 blanchet clean up new Skolemizer code -- some old hacks are no longer necessary
Thu, 24 Mar 2011 17:49:27 +0100 blanchet remove newly added wrong logic
Thu, 24 Mar 2011 17:49:27 +0100 blanchet avoid evil "export_without_context", which breaks if there are local "fixes"
Thu, 24 Mar 2011 17:49:27 +0100 blanchet more robust handling of variables in new Skolemizer
Mon, 10 Jan 2011 15:45:46 +0100 wenzelm eliminated Int.toString;
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"
Wed, 15 Dec 2010 11:26:28 +0100 blanchet added Sledgehammer support for higher-order propositional reasoning
Wed, 15 Dec 2010 11:26:28 +0100 blanchet add Metis support for higher-order propositional reasoning
Wed, 15 Dec 2010 11:26:28 +0100 blanchet tuning: unused var
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)
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
Tue, 23 Nov 2010 18:26:56 +0100 blanchet added "verbose" option to Metis to shut up its warnings if necessary
Fri, 29 Oct 2010 12:49:05 +0200 blanchet fixed order of quantifier instantiation in new Skolemizer
less more (0) -60 tip