src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
Thu, 26 Jun 2014 13:36:13 +0200 blanchet tuning
Thu, 26 Jun 2014 13:36:06 +0200 blanchet refactoring
Thu, 26 Jun 2014 13:36:00 +0200 blanchet removed experimental machine learning engine
Thu, 26 Jun 2014 13:35:56 +0200 blanchet store string-to-index tables in memory
Thu, 26 Jun 2014 13:35:52 +0200 blanchet disable 'extra' feature tainting for now
Thu, 26 Jun 2014 13:35:46 +0200 blanchet tuning
Thu, 26 Jun 2014 13:35:39 +0200 blanchet tuning
Thu, 26 Jun 2014 13:35:36 +0200 blanchet tuning
Thu, 26 Jun 2014 13:35:30 +0200 blanchet tuning
Thu, 26 Jun 2014 13:35:21 +0200 blanchet tuning
Thu, 26 Jun 2014 13:35:17 +0200 blanchet honor visible in SML naive Bayes
Thu, 26 Jun 2014 13:35:12 +0200 blanchet honor visibility in SML k-NN
Thu, 26 Jun 2014 13:35:07 +0200 blanchet got rid of a few experimental options
Thu, 26 Jun 2014 13:35:00 +0200 blanchet tuning
Thu, 26 Jun 2014 13:34:57 +0200 blanchet killed dead code
Thu, 26 Jun 2014 13:34:50 +0200 blanchet avoid subscripting array with ~1
Thu, 26 Jun 2014 13:34:39 +0200 blanchet killed dead data
Thu, 26 Jun 2014 13:34:28 +0200 blanchet new version of adaptive k-NN with TFIDF
Thu, 26 Jun 2014 13:33:50 +0200 blanchet refactoring
Thu, 26 Jun 2014 13:33:27 +0200 blanchet tuning
Thu, 26 Jun 2014 13:33:21 +0200 blanchet refactoring
Thu, 26 Jun 2014 13:33:08 +0200 blanchet adaptive k-NN
Tue, 24 Jun 2014 15:08:19 +0200 blanchet optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
Tue, 24 Jun 2014 14:56:08 +0200 blanchet minor table access optimization
Tue, 24 Jun 2014 12:36:45 +0200 blanchet optimize log
Tue, 24 Jun 2014 12:35:57 +0200 blanchet enable TF-IDF
Tue, 24 Jun 2014 12:35:49 +0200 blanchet added another experimental engine
Tue, 24 Jun 2014 12:35:43 +0200 blanchet tweaked experimental setup
Tue, 24 Jun 2014 08:19:58 +0200 blanchet use strings to communicate with external process, to ease debugging
Tue, 24 Jun 2014 08:19:55 +0200 blanchet added experimental MaSh engine
Fri, 20 Jun 2014 09:55:31 +0200 blanchet changed default MaSh parameters based on (in vitro) evaluation
Wed, 18 Jun 2014 17:42:24 +0200 blanchet more MaSh engine variations, for evaluations
Wed, 18 Jun 2014 17:42:24 +0200 blanchet split parameter into two
Wed, 18 Jun 2014 15:23:40 +0200 blanchet more generous formula -- there are lots of duplicates out there
Wed, 18 Jun 2014 14:19:42 +0200 blanchet automatically learn MaSh facts also in 'blocking' mode
Mon, 02 Jun 2014 11:59:50 +0200 blanchet add option to keep duplicates, for more precise evaluation of relevance filters
Fri, 30 May 2014 16:00:54 +0200 blanchet made 'Kuehlwein-style' be really like Python code, we now think
Fri, 30 May 2014 15:15:41 +0200 blanchet make SML code closer to Python code when 'nb_kuehlwein_style' is true
Fri, 30 May 2014 14:43:06 +0200 blanchet added sleep to give time for the server to shut down -- this is a hack, but it's only in experimental code that will hopefully soon go away
Fri, 30 May 2014 12:27:51 +0200 blanchet added another way of invoking Python code, for experiments
Fri, 30 May 2014 12:27:51 +0200 blanchet make SML naive Bayes closer to Python version
Fri, 30 May 2014 12:27:51 +0200 blanchet more work on exporter
Fri, 30 May 2014 12:27:51 +0200 blanchet extend exporter with new versions of MaSh
Wed, 28 May 2014 17:42:36 +0200 blanchet more generous max number of suggestions, for more safety
Wed, 28 May 2014 17:42:34 +0200 blanchet changed MaSh to use SML version instead of Python version of naive Bayes by default (i.e. if MASH=yes in the settings, or 'fact_filter=mash' with no other explicit setting)
Wed, 28 May 2014 17:42:33 +0200 blanchet export more ML functions, for experimentation
Wed, 28 May 2014 14:02:49 +0200 blanchet disabled IDF for now -- empirical evidence points the wrong way (as usual)
Wed, 28 May 2014 13:31:44 +0200 blanchet tuning
Wed, 28 May 2014 13:02:47 +0200 blanchet tuning
Wed, 28 May 2014 12:34:26 +0200 blanchet optimized computation
Wed, 28 May 2014 10:04:28 +0200 blanchet enabled IDF for naive Bayes ML
Wed, 28 May 2014 10:03:14 +0200 blanchet tuning
Wed, 28 May 2014 09:44:14 +0200 blanchet repaired subscript problem in SML kNN
Wed, 28 May 2014 09:38:39 +0200 blanchet tuning
Wed, 28 May 2014 03:10:30 +0200 blanchet always remove duplicates in meshing + use weights for Naive Bayes
Tue, 27 May 2014 17:48:11 +0200 blanchet updated naive Bayes
Mon, 26 May 2014 14:15:48 +0200 blanchet renamed 'MaSh' option
Fri, 23 May 2014 14:12:20 +0200 blanchet automatically reload state file when it changes on disk
Thu, 22 May 2014 14:27:43 +0200 blanchet avoid slow inspection of proof terms now that dependencies are stored in 'state'
Thu, 22 May 2014 13:46:49 +0200 blanchet properly mark relearns as dirty
less more (0) -100 -60 tip