--- a/CONTRIBUTORS Mon Nov 26 12:13:37 2012 +0100
+++ b/CONTRIBUTORS Mon Nov 26 13:35:05 2012 +0100
@@ -9,6 +9,10 @@
* 2012: Makarius Wenzel, Université Paris-Sud / LRI
Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
+* Fall 2012: Daniel Kuehlwein, ICIS, Radboud University Nijmegen
+ Jasmin Blanchette, TUM
+ Implemented Machine Learning for Sledgehammer (MaSh).
+
* Fall 2012: Steffen Smolka, TUM
Various improvements to Sledgehammer's Isar proof generator, including
a smart type annotation algorithm and proof shrinking.
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/argparse.py Mon Nov 26 12:13:37 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/argparse.py Mon Nov 26 13:35:05 2012 +0100
@@ -1,3 +1,7 @@
+# Title: HOL/Tools/Sledgehammer/MaSh/src/argparse.py
+#
+# Argument parser. See copyright notice below.
+
# -*- coding: utf-8 -*-
# Copyright © 2006-2009 Steven J. Bethard <steven.bethard@gmail.com>.
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py Mon Nov 26 12:13:37 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py Mon Nov 26 13:35:05 2012 +0100
@@ -1,4 +1,10 @@
#!/usr/bin/python
+# Title: HOL/Tools/Sledgehammer/MaSh/src/compareStats.py
+# Author: Daniel Kuehlwein, ICIS, Radboud University Nijmegen
+# Copyright 2012
+#
+# Tool that compares MaSh statistics and displays a comparison.
+
'''
Created on Jul 13, 2012
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py Mon Nov 26 12:13:37 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py Mon Nov 26 13:35:05 2012 +0100
@@ -1,3 +1,9 @@
+# Title: HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py
+# Author: Daniel Kuehlwein, ICIS, Radboud University Nijmegen
+# Copyright 2012
+#
+# Persistent dictionaries: accessibility, dependencies, and features.
+
'''
Created on Jul 12, 2012
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py Mon Nov 26 12:13:37 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py Mon Nov 26 13:35:05 2012 +0100
@@ -1,4 +1,10 @@
#!/usr/bin/python
+# Title: HOL/Tools/Sledgehammer/MaSh/src/mash.py
+# Author: Daniel Kuehlwein, ICIS, Radboud University Nijmegen
+# Copyright 2012
+#
+# Entry point for MaSh (Machine Learning for Sledgehammer).
+
'''
MaSh - Machine Learning for Sledgehammer
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/naiveBayes.py Mon Nov 26 12:13:37 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/naiveBayes.py Mon Nov 26 13:35:05 2012 +0100
@@ -1,3 +1,9 @@
+# Title: HOL/Tools/Sledgehammer/MaSh/src/naiveBayes.py
+# Author: Daniel Kuehlwein, ICIS, Radboud University Nijmegen
+# Copyright 2012
+#
+# An updatable naive Bayes classifier.
+
'''
Created on Jul 11, 2012
@@ -10,7 +16,7 @@
class NBClassifier(object):
'''
- An updateable naive Bayes classifier.
+ An updatable naive Bayes classifier.
'''
def __init__(self):
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/predefined.py Mon Nov 26 12:13:37 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/predefined.py Mon Nov 26 13:35:05 2012 +0100
@@ -1,3 +1,9 @@
+# Title: HOL/Tools/Sledgehammer/MaSh/src/predefined.py
+# Author: Daniel Kuehlwein, ICIS, Radboud University Nijmegen
+# Copyright 2012
+#
+# A classifier that uses the Meng-Paulson predictions.
+
'''
Created on Jul 11, 2012
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/readData.py Mon Nov 26 12:13:37 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/readData.py Mon Nov 26 13:35:05 2012 +0100
@@ -1,3 +1,9 @@
+# Title: HOL/Tools/Sledgehammer/MaSh/src/readData.py
+# Author: Daniel Kuehlwein, ICIS, Radboud University Nijmegen
+# Copyright 2012
+#
+# All functions to read the Isabelle output.
+
'''
All functions to read the Isabelle output.
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/snow.py Mon Nov 26 12:13:37 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/snow.py Mon Nov 26 13:35:05 2012 +0100
@@ -1,3 +1,9 @@
+# Title: HOL/Tools/Sledgehammer/MaSh/src/snow.py
+# Author: Daniel Kuehlwein, ICIS, Radboud University Nijmegen
+# Copyright 2012
+#
+# Wrapper for SNoW.
+
'''
THIS FILE IS NOT UP TO DATE!
NEEDS SOME FIXING BEFORE IT WILL WORK WITH THE MAIN ALGORITHM
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/stats.py Mon Nov 26 12:13:37 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/stats.py Mon Nov 26 13:35:05 2012 +0100
@@ -1,3 +1,9 @@
+# Title: HOL/Tools/Sledgehammer/MaSh/src/stats.py
+# Author: Daniel Kuehlwein, ICIS, Radboud University Nijmegen
+# Copyright 2012
+#
+# Statistics collector.
+
'''
Created on Jul 9, 2012