src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
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
Mon, 05 Sep 2011 14:42:31 +0200 blanchet fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
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)
Tue, 30 Aug 2011 16:07:45 +0200 blanchet extended simple types with polymorphism -- the implementation still needs some work though
Thu, 25 Aug 2011 14:25:07 +0200 blanchet rationalized option names -- mono becomes raw_mono and mangled becomes mono
Wed, 24 Aug 2011 11:17:33 +0200 blanchet more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
Mon, 22 Aug 2011 15:02:45 +0200 blanchet cleaner handling of polymorphic monotonicity inference
Tue, 09 Aug 2011 09:33:50 +0200 blanchet renamed E wrappers for consistency with CASC conventions
Tue, 26 Jul 2011 22:53:06 +0200 blanchet renamed "preds" encodings to "guards"
Fri, 01 Jul 2011 15:53:38 +0200 blanchet renamed "type_sys" to "type_enc", which is more accurate
Mon, 27 Jun 2011 14:56:28 +0200 blanchet added "sound" option to force Sledgehammer to be pedantically sound
Mon, 27 Jun 2011 13:52:47 +0200 blanchet removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
Fri, 10 Jun 2011 12:01:15 +0200 blanchet removed "atp" and "atps" aliases, which users should have forgotten by now if they ever used them
Fri, 10 Jun 2011 12:01:15 +0200 blanchet fewer monomorphic instances are necessary, thanks to Sascha's new monomorphizer -- backed up by Judgment Day
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"
Tue, 31 May 2011 16:38:36 +0200 blanchet parse optional type system specification
less more (0) -100 -60 tip