src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
Fri, 11 Jan 2013 14:35:28 +0100 smolkas tuned
Fri, 11 Jan 2013 13:57:51 +0100 smolkas set show_markup to false in order to avoid problems in jedit
Sat, 05 Jan 2013 22:31:30 +0100 blanchet nicer output
Sat, 05 Jan 2013 22:31:30 +0100 blanchet pass option to minimize
Fri, 04 Jan 2013 19:00:49 +0100 blanchet renamed "kill" subcommand to avoid clash with "kill" keyword (which confuses Proof General and results in strange syntax highlighting)
Wed, 19 Dec 2012 22:43:07 +0100 blanchet crank up default timeout for MaSh ATP learning
Sat, 15 Dec 2012 19:57:12 +0100 blanchet thread no timeout properly
Wed, 12 Dec 2012 00:24:06 +0100 blanchet adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
Mon, 12 Nov 2012 14:11:51 +0100 blanchet create temp directory if not already created
Tue, 06 Nov 2012 15:15:33 +0100 blanchet renamed Sledgehammer option
Thu, 18 Oct 2012 15:05:17 +0200 blanchet renamed Isar-proof related options + changed semantics of Isar shrinking
Fri, 28 Sep 2012 09:12:50 +0200 blanchet tuned message
Fri, 14 Sep 2012 12:09:27 +0200 blanchet merged two commands
Thu, 26 Jul 2012 11:07:27 +0200 blanchet detect unknown options again
Mon, 23 Jul 2012 15:32:30 +0200 blanchet don't relearn old facts in Isar mode
Mon, 23 Jul 2012 15:32:30 +0200 blanchet took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks
Fri, 20 Jul 2012 22:19:46 +0200 blanchet honor suggested MaSh weights
Fri, 20 Jul 2012 22:19:46 +0200 blanchet use CVC3 and Yices by default if they are available and there are enough cores
Fri, 20 Jul 2012 22:19:46 +0200 blanchet minimal maxes + tuning
Fri, 20 Jul 2012 22:19:46 +0200 blanchet learn from SMT proofs when they can be minimized by Metis
Fri, 20 Jul 2012 22:19:46 +0200 blanchet convenience
Fri, 20 Jul 2012 22:19:46 +0200 blanchet learning should honor the fact override and the chained facts
Fri, 20 Jul 2012 22:19:46 +0200 blanchet added "learn_from_atp" command to MaSh, for patient users
Fri, 20 Jul 2012 22:19:46 +0200 blanchet more MaSh docs
Fri, 20 Jul 2012 22:19:46 +0200 blanchet learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
Fri, 20 Jul 2012 22:19:46 +0200 blanchet learn command in MaSh
Fri, 20 Jul 2012 22:19:45 +0200 blanchet renamed ML structures
Wed, 18 Jul 2012 08:44:05 +0200 blanchet optimize parent computation in MaSh + remove temporary files
Wed, 18 Jul 2012 08:44:04 +0200 blanchet learn from minimized ATP proofs
Wed, 18 Jul 2012 08:44:04 +0200 blanchet use async manager to manage MaSh learners to make sure they get killed cleanly
Wed, 18 Jul 2012 08:44:04 +0200 blanchet added option to control which fact filter is used
Wed, 18 Jul 2012 08:44:04 +0200 blanchet make tracing an option
Wed, 18 Jul 2012 08:44:03 +0200 blanchet more implementation work on MaSh
Wed, 18 Jul 2012 08:44:03 +0200 blanchet started implementing MaSh client-side I/O
Wed, 18 Jul 2012 08:44:03 +0200 blanchet renamed Sledgehammer options
Wed, 18 Jul 2012 08:44:03 +0200 blanchet more code rationalization in relevance filter
Wed, 11 Jul 2012 21:43:19 +0200 blanchet further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
Wed, 23 May 2012 13:28:20 +0200 blanchet lower the monomorphization thresholds for less scalable provers
Sat, 21 Apr 2012 11:15:49 +0200 blanchet swap out Satallax, pull in E-SInE again -- it's not clear yet how useful Satallax is after proof reconstruction, whereas E-SInE performed surprisingly well on latest evaluations
Wed, 21 Mar 2012 16:53:24 +0100 blanchet improve "remote_satallax" by exploiting unsat core
Tue, 20 Mar 2012 18:42:45 +0100 blanchet made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
Tue, 20 Mar 2012 00:44:30 +0100 blanchet added "dont_preplay" alias
Fri, 16 Mar 2012 18:20:12 +0100 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations;
Thu, 15 Mar 2012 20:07:00 +0100 wenzelm prefer formally checked @{keyword} parser;
Mon, 06 Feb 2012 23:01:01 +0100 blanchet renamed type encoding
Sat, 04 Feb 2012 12:08:18 +0100 blanchet made option available to users (mostly for experiments)
Thu, 02 Feb 2012 12:42:05 +0100 blanchet include new SPASS by default if available
Mon, 23 Jan 2012 17:40:32 +0100 blanchet renamed two files to make room for a new file
Thu, 19 Jan 2012 21:37:12 +0100 blanchet renamed "sound" option to "strict"
Thu, 19 Jan 2012 21:37:12 +0100 blanchet lower timeout for preplay, now that we have more preplay methods
Thu, 01 Dec 2011 13:34:14 +0100 blanchet added "minimize" option for more control over automatic minimization
Thu, 01 Dec 2011 13:34:13 +0100 blanchet renamed "slicing" to "slice"
Wed, 16 Nov 2011 16:35:19 +0100 blanchet thread in additional options to minimizer
Wed, 16 Nov 2011 13:22:36 +0100 blanchet make metis reconstruction handling more flexible
Wed, 16 Nov 2011 09:42:27 +0100 blanchet parse lambda translation option in Metis
Fri, 23 Sep 2011 16:44:51 +0200 blanchet reintroduced E-SInE now that it's unexpectedly working again (thanks to Geoff)
Thu, 22 Sep 2011 19:42:06 +0200 blanchet take out remote E-SInE -- it's broken and Geoff says it might take quite a while before he gets to it, plus it's fairly obsolete in the meantime
Wed, 07 Sep 2011 13:50:17 +0200 blanchet parse new experimental '@' encodings
Wed, 07 Sep 2011 13:50:17 +0200 blanchet tuning
Wed, 07 Sep 2011 09:10:41 +0200 blanchet rationalize uniform encodings
less more (0) -100 -60 tip