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_reconstruct.ML
Tue, 26 Jun 2012 11:14:39 +0200 blanchet added type arguments to "ATerm" constructor -- but don't use them yet file | diff | annotate
Mon, 27 Feb 2012 15:48:02 +0100 wenzelm prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required; file | diff | annotate
Thu, 02 Feb 2012 01:20:28 +0100 blanchet implemented partial application aliases (for SPASS mainly) file | diff | annotate
Mon, 23 Jan 2012 17:40:32 +0100 blanchet renamed two files to make room for a new file file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet wrap lambdas earlier, to get more control over beta/eta file | diff | annotate
Tue, 15 Nov 2011 22:13:39 +0100 blanchet continued implementation of lambda-lifting in Metis file | diff | annotate
Tue, 15 Nov 2011 22:13:39 +0100 blanchet started implementing lambda-lifting in Metis file | diff | annotate
Thu, 25 Aug 2011 14:25:07 +0200 blanchet avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics file | diff | annotate
Wed, 17 Aug 2011 18:05:31 +0200 wenzelm modernized signature of Term.absfree/absdummy; file | diff | annotate
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy; file | diff | annotate
Fri, 10 Jun 2011 17:52:09 +0200 blanchet tuning file | diff | annotate
Thu, 09 Jun 2011 23:12:02 +0200 wenzelm renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate; file | diff | annotate
Thu, 09 Jun 2011 20:56:08 +0200 wenzelm clarified special incr_type_indexes; 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 removed more dead code 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
Wed, 08 Jun 2011 22:13:49 +0200 wenzelm merged file | diff | annotate
Wed, 08 Jun 2011 16:20:18 +0200 blanchet restore comment about subtle issue file | diff | annotate
Wed, 08 Jun 2011 15:56:57 +0200 wenzelm more robust exception pattern General.Subscript; file | diff | annotate
Wed, 08 Jun 2011 08:47:43 +0200 blanchet removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name" file | diff | annotate
Wed, 08 Jun 2011 08:47:43 +0200 blanchet removed experimental code submitted by mistake file | diff | annotate
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" file | diff | annotate
Tue, 07 Jun 2011 10:43:18 +0200 blanchet nicely thread monomorphism verbosity in Metis and Sledgehammer file | diff | annotate
Mon, 06 Jun 2011 20:56:06 +0200 blanchet Metis code cleanup file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet fall back in case path finder fails -- these errors are sometimes salvageable 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 improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis) file | diff | annotate
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) file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet tuning 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:35 +0200 blanchet properly unmangle names in path finder 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:34 +0200 blanchet added Metis examples to test the new 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 implemented missing hAPP and ti cases of new path finder 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 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
less more (0) -60 tip
isabelle