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_tactic.ML
Mon, 16 Jun 2014 19:40:59 +0200 blanchet simplified code file | diff | annotate
Sun, 16 Feb 2014 21:33:28 +0100 blanchet removed final periods in messages for proof methods file | diff | annotate
Sun, 16 Feb 2014 18:46:13 +0100 blanchet added a version of the Metis tactic that returns the unused facts file | diff | annotate
Sun, 16 Feb 2014 18:39:42 +0100 blanchet tuned code file | diff | annotate
Tue, 04 Feb 2014 01:35:48 +0100 blanchet removed legacy 'metisFT' method file | diff | annotate
Mon, 03 Feb 2014 15:19:07 +0100 blanchet merged 'reconstructors' and 'proof methods' file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet rationalized threading of 'metis' arguments file | diff | annotate
Sat, 01 Feb 2014 21:09:53 +0100 wenzelm more standard file/module names; file | diff | annotate
Sat, 01 Feb 2014 18:42:46 +0100 wenzelm proper context for printing; file | diff | annotate
Thu, 02 Jan 2014 19:07:36 +0100 blanchet removed pointless warning (cf. http://stackoverflow.com/questions/20233463/isabelle-metis-proof-state-contains-the-universal-sort/20785045#20785045) file | diff | annotate
Tue, 31 Dec 2013 14:29:16 +0100 wenzelm proper context for norm_hhf and derived operations; file | diff | annotate
Sun, 15 Dec 2013 18:54:26 +0100 blanchet tuning file | diff | annotate
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; file | diff | annotate
Tue, 19 Nov 2013 17:37:35 +0100 blanchet refactoring file | diff | annotate
Sat, 27 Jul 2013 16:35:51 +0200 wenzelm standardized aliases; file | diff | annotate
Thu, 16 May 2013 13:34:13 +0200 blanchet tuning -- renamed '_from_' to '_of_' in Sledgehammer file | diff | annotate
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset; file | diff | annotate
Mon, 14 Jan 2013 09:59:50 +0100 blanchet less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2 file | diff | annotate
Thu, 03 Jan 2013 17:28:55 +0100 blanchet use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments) file | diff | annotate
Thu, 03 Jan 2013 09:56:39 +0100 blanchet avoid repeated calls to metis from "resolve_tac" in case of ultimate failure file | diff | annotate
Tue, 20 Mar 2012 13:53:09 +0100 blanchet more conservative Metis defaults, for backward compatiblity (as illustrated by one "metis" call in "Auth/KerberosV") file | diff | annotate
Tue, 20 Mar 2012 13:53:09 +0100 blanchet enable "metis_advisory_simp" by default file | diff | annotate
Tue, 20 Mar 2012 10:06:35 +0100 blanchet added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle") file | diff | annotate
Mon, 19 Mar 2012 12:43:46 +0100 blanchet better defaults for Metis, that seem to make it less likely to loop seemingly forever -- 0 coefficients might very well make it incomplete file | diff | annotate
Thu, 15 Mar 2012 20:07:00 +0100 wenzelm prefer formally checked @{keyword} parser; file | diff | annotate
Tue, 13 Mar 2012 16:40:06 +0100 wenzelm prefer abs_def over def_raw; file | diff | annotate
Mon, 30 Jan 2012 17:15:59 +0100 blanchet rename lambda translation schemes 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
Thu, 19 Jan 2012 21:37:12 +0100 blanchet renamed "sound" option to "strict" file | diff | annotate
Wed, 14 Dec 2011 23:08:03 +0100 blanchet killed dead code file | diff | annotate
Fri, 18 Nov 2011 14:47:08 +0100 blanchet more robust options file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones 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
Fri, 18 Nov 2011 11:47:12 +0100 blanchet move eta-contraction to before translation to Metis, to ensure everything stays in sync file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet avoid that var names get changed by resolution in Metis lambda-lifting file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet avoid spurious messages in "lam_lifting" mode file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet eta-contract to avoid needless "lambda" wrappers file | diff | annotate
Wed, 16 Nov 2011 17:06:14 +0100 blanchet give each time slice its own lambda translation file | diff | annotate
Wed, 16 Nov 2011 13:22:36 +0100 blanchet make metis reconstruction handling more flexible file | diff | annotate
Wed, 16 Nov 2011 09:42:27 +0100 blanchet parse lambda translation option in Metis file | diff | annotate
Tue, 15 Nov 2011 22:20:58 +0100 blanchet rename the lambda translation schemes, so that they are understandable out of context file | diff | annotate
Tue, 15 Nov 2011 22:15:51 +0100 blanchet rename configuration option to more reasonable length 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, 22 Sep 2011 16:30:47 +0200 blanchet better type reconstruction -- prevents ill-instantiations in proof replay file | diff | annotate
Thu, 15 Sep 2011 10:57:40 +0200 blanchet tuning file | diff | annotate
Wed, 07 Sep 2011 09:10:41 +0200 blanchet rationalize uniform encodings file | diff | annotate
Fri, 02 Sep 2011 14:43:20 +0200 blanchet renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy) file | diff | annotate | base
less more (0) tip
isabelle