Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
Thu, 26 Jan 2012 20:49:54 +0100 blanchet separate orthogonal components 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
Thu, 19 Jan 2012 21:37:12 +0100 blanchet cleanly separate each Metis encoding file | diff | annotate
Wed, 07 Dec 2011 16:03:05 +0100 blanchet use same order of facts for preplay as for actual reconstruction -- Metis sometimes exhibits very different timings depending on the order of the facts file | diff | annotate
Thu, 01 Dec 2011 13:34:14 +0100 blanchet added "minimize" option for more control over automatic minimization file | diff | annotate
Thu, 01 Dec 2011 13:34:13 +0100 blanchet renamed "slicing" to "slice" file | diff | annotate
Sat, 19 Nov 2011 12:42:21 +0100 blanchet made SML/NJ happy file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet be more silent when auto minimizing file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet better threading of type encodings between Sledgehammer and "metis" file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet don't propagate user-set "type_enc" or "lam_trans" to Metis calls file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet don't needlessly pass "lam_lifted" option to "metis" call for SMT proof file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet quiet down SMT file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet more aggressive lambda hiding (if we anyway need to pass an option to Metis) file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet don't pass "lam_lifted" option to "metis" unless there's a good reason file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet no needless reconstructors file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet removed more clutter file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet removed needless baggage 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 16:35:19 +0100 blanchet thread in additional options to minimizer 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:15:51 +0100 blanchet rename configuration option to more reasonable length file | diff | annotate
Tue, 15 Nov 2011 22:13:39 +0100 blanchet started implementing lambda-lifting in Metis file | diff | annotate
Sun, 06 Nov 2011 22:18:54 +0100 blanchet more millisecond cleanup file | diff | annotate
Sun, 06 Nov 2011 22:18:54 +0100 blanchet try "smt" as a fallback for ATPs if "metis" fails/times out file | diff | annotate
Sun, 06 Nov 2011 22:18:54 +0100 blanchet more detailed preplay output file | diff | annotate
Sun, 06 Nov 2011 22:18:54 +0100 blanchet tuning file | diff | annotate
Sun, 06 Nov 2011 13:57:17 +0100 blanchet use "Time.time" rather than milliseconds internally file | diff | annotate
Sun, 06 Nov 2011 13:46:26 +0100 blanchet tune: no need for option file | diff | annotate
Sat, 29 Oct 2011 13:15:58 +0200 blanchet added DFG unsorted support (like in the old days) file | diff | annotate
Sat, 29 Oct 2011 13:15:58 +0200 blanchet added sorted DFG output for coming version of SPASS file | diff | annotate
Sat, 29 Oct 2011 13:15:58 +0200 blanchet check "sound" flag before doing something unsound... file | diff | annotate
Tue, 13 Sep 2011 11:24:58 +0200 blanchet simplified unsound proof detection by removing impossible case file | diff | annotate
Sat, 10 Sep 2011 00:44:25 +0200 blanchet continue with minimization in debug mode in spite of unsoundness 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
Fri, 02 Sep 2011 14:43:20 +0200 blanchet fewer TPTP important messages file | diff | annotate
Thu, 01 Sep 2011 13:18:27 +0200 blanchet always measure time for ATPs -- auto minimization relies on it file | diff | annotate
Thu, 01 Sep 2011 13:18:27 +0200 blanchet make "sound" sound and "unsound" more sound, based on evaluation file | diff | annotate
Tue, 30 Aug 2011 16:25:10 +0200 blanchet fixed just introduced silly bug file | diff | annotate
Tue, 30 Aug 2011 16:11:42 +0200 blanchet tuning file | diff | annotate
Tue, 30 Aug 2011 16:07:45 +0200 blanchet flip logic of boolean option so it's off by default file | diff | annotate
Tue, 30 Aug 2011 14:12:55 +0200 nik improved handling of induction rules in Sledgehammer file | diff | annotate
Tue, 30 Aug 2011 14:12:55 +0200 nik added generation of induction rules file | diff | annotate
Fri, 26 Aug 2011 10:25:13 +0200 blanchet added a component in generated file names reflecting whether the minimizer is used -- needed for evaluation to keep these files separated from the main problem files file | diff | annotate
Tue, 23 Aug 2011 16:07:01 +0200 blanchet exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp" file | diff | annotate
Tue, 23 Aug 2011 14:44:19 +0200 blanchet added formats to the slice and use TFF for remote Vampire file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet cleaner handling of polymorphic monotonicity inference file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet added option to control soundness of encodings more precisely, for evaluation purposes file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet make sound mode more sound (and clean up code) file | diff | annotate
Tue, 09 Aug 2011 09:05:22 +0200 blanchet move lambda-lifting code to ATP encoding, so it can be used by Metis file | diff | annotate
Thu, 28 Jul 2011 11:43:45 +0200 blanchet tuning file | diff | annotate
Tue, 26 Jul 2011 14:53:00 +0200 blanchet remove spurious message file | diff | annotate
Mon, 25 Jul 2011 14:10:12 +0200 blanchet introduced hybrid lambda translation file | diff | annotate
Mon, 25 Jul 2011 14:10:12 +0200 blanchet avoid needless type args for lifted-lambdas file | diff | annotate
Thu, 21 Jul 2011 21:29:10 +0200 blanchet make "concealed" lambda translation sound file | diff | annotate
Wed, 20 Jul 2011 23:47:27 +0200 blanchet use a more robust naming convention for "polymorphic" frees -- the check is an overapproximation but that's fine as far as soundness is concerned file | diff | annotate
Wed, 20 Jul 2011 12:23:20 +0200 boehmes generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code) file | diff | annotate
Wed, 20 Jul 2011 09:23:12 +0200 boehmes moved lambda-lifting on terms into a separate structure (for better re-use in tools other than SMT) file | diff | annotate
Sun, 17 Jul 2011 14:21:19 +0200 blanchet fixed lambda-liftg: must ensure the formulas are in close form file | diff | annotate
less more (0) -100 -60 tip
isabelle