Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -300 -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
Fri, 16 May 2014 19:13:50 +0200 blanchet use 'simp add:' syntax in Sledgehammer rather than 'using' file | diff | annotate
Sun, 04 May 2014 19:01:36 +0200 blanchet added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0') file | diff | annotate
Fri, 14 Mar 2014 11:44:11 +0100 blanchet consolidate consecutive steps that prove the same formula file | diff | annotate
Fri, 14 Mar 2014 11:15:46 +0100 blanchet undo rewrite rules (e.g. for 'fun_app') in Isar file | diff | annotate
Fri, 14 Mar 2014 11:05:45 +0100 blanchet debugging stuff file | diff | annotate
Fri, 14 Mar 2014 11:05:44 +0100 blanchet more simplification of trivial steps file | diff | annotate
Fri, 14 Mar 2014 11:05:37 +0100 blanchet tuning file | diff | annotate
Thu, 13 Mar 2014 13:18:14 +0100 blanchet tuning file | diff | annotate
Thu, 13 Mar 2014 13:18:14 +0100 blanchet simplified preplaying information file | diff | annotate
Thu, 13 Mar 2014 13:18:13 +0100 blanchet integrate SMT2 with Sledgehammer file | diff | annotate
Thu, 06 Mar 2014 10:12:47 +0100 wenzelm tuned signature; file | diff | annotate
Thu, 13 Feb 2014 13:16:17 +0100 blanchet avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures file | diff | annotate
Tue, 04 Feb 2014 23:11:18 +0100 blanchet more generous Isar proof compression -- try to remove failing steps file | diff | annotate
Tue, 04 Feb 2014 23:11:18 +0100 blanchet do a second phase of proof compression after minimization file | diff | annotate
Tue, 04 Feb 2014 23:11:18 +0100 blanchet tuned code file | diff | annotate
Tue, 04 Feb 2014 23:11:18 +0100 blanchet split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed) file | diff | annotate
Mon, 03 Feb 2014 23:59:36 +0100 blanchet rationalized lists of methods file | diff | annotate
Mon, 03 Feb 2014 23:49:01 +0100 blanchet extended method list file | diff | annotate
Mon, 03 Feb 2014 19:32:02 +0100 blanchet generate comments in Isar proofs file | diff | annotate
Mon, 03 Feb 2014 19:32:02 +0100 blanchet renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover file | diff | annotate
Mon, 03 Feb 2014 19:32:02 +0100 blanchet tuned behavior of 'smt' option file | diff | annotate
Mon, 03 Feb 2014 19:32:02 +0100 blanchet proper fresh name generation file | diff | annotate
Mon, 03 Feb 2014 17:13:31 +0100 blanchet added 'smt' option to control generation of 'by smt' proofs file | diff | annotate
Mon, 03 Feb 2014 16:53:58 +0100 blanchet renamed ML file file | diff | annotate
Mon, 03 Feb 2014 15:33:18 +0100 blanchet tuning file | diff | annotate
Mon, 03 Feb 2014 15:19:07 +0100 blanchet merged 'reconstructors' and 'proof methods' file | diff | annotate
Mon, 03 Feb 2014 13:37:23 +0100 blanchet tuning file | diff | annotate
Mon, 03 Feb 2014 11:58:38 +0100 blanchet tuned data structure file | diff | annotate
Mon, 03 Feb 2014 11:37:48 +0100 blanchet tuned data structure file | diff | annotate
Mon, 03 Feb 2014 10:14:18 +0100 blanchet less aggressive evaluation file | diff | annotate
Mon, 03 Feb 2014 10:14:18 +0100 blanchet added a new version of 'metis' to the mix file | diff | annotate
Mon, 03 Feb 2014 10:14:18 +0100 blanchet implemented new 'try0_isar' semantics file | diff | annotate
Mon, 03 Feb 2014 10:14:18 +0100 blanchet got rid of 'try0' step that is now redundant file | diff | annotate
Mon, 03 Feb 2014 10:14:18 +0100 blanchet centralize more preplaying file | diff | annotate
Mon, 03 Feb 2014 10:14:18 +0100 blanchet centralize preplaying file | diff | annotate
Mon, 03 Feb 2014 10:14:18 +0100 blanchet tuned file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet more data structure rationalization file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet more data structure rationalization file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet rationalized threading of 'metis' arguments file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet refactored data structure (step 3) file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet unform treatment of preplay_timeout = 0 and > 0 file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet use Skolem proof methods appropriately file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods file | diff | annotate
Fri, 31 Jan 2014 19:16:41 +0100 blanchet generalized preplaying infrastructure to store various results for various methods file | diff | annotate
Fri, 31 Jan 2014 18:43:16 +0100 blanchet added a 'trace' option file | diff | annotate
Fri, 31 Jan 2014 18:43:16 +0100 blanchet moved code around file | diff | annotate
Fri, 31 Jan 2014 18:43:16 +0100 blanchet added 'algebra' to the mix file | diff | annotate
Fri, 31 Jan 2014 18:43:16 +0100 blanchet more informative trace file | diff | annotate
Fri, 31 Jan 2014 16:41:54 +0100 blanchet better tracing + syntactically correct 'metis' calls file | diff | annotate
Fri, 31 Jan 2014 16:26:43 +0100 blanchet tuned ML function names file | diff | annotate
Fri, 31 Jan 2014 16:10:39 +0100 blanchet tuning file | diff | annotate
Fri, 31 Jan 2014 16:07:20 +0100 blanchet moved ML code around file | diff | annotate
Fri, 31 Jan 2014 10:23:32 +0100 blanchet renamed many Sledgehammer ML files to clarify structure file | diff | annotate | base
Thu, 30 Jan 2014 14:37:53 +0100 blanchet renamed Sledgehammer options for symmetry between positive and negative versions file | diff | annotate
Thu, 19 Dec 2013 13:43:21 +0100 blanchet made timeouts in Sledgehammer not be 'option's -- simplified lots of code file | diff | annotate
Thu, 21 Nov 2013 12:29:29 +0100 blanchet fixed spying so that the envirnoment variables are queried at run-time not at build-time file | diff | annotate
Tue, 19 Nov 2013 18:34:04 +0100 blanchet tuning file | diff | annotate
Thu, 17 Oct 2013 01:34:34 +0200 blanchet added comment file | diff | annotate
Tue, 15 Oct 2013 15:31:18 +0200 blanchet use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available file | diff | annotate
Fri, 04 Oct 2013 11:52:10 +0200 blanchet run fewer provers in "try" mode file | diff | annotate
less more (0) -300 -100 -60 tip
isabelle