# HG changeset patch
# User blanchet
# Date 1353933305 -3600
# Node ID 40e3c3be6bcaa302e655338897473f9accaef942
# Parent  355aaa57ac3917b66b1d04ce1733281963e53bce
added file headers

diff -r 355aaa57ac39 -r 40e3c3be6bca CONTRIBUTORS
--- 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.
diff -r 355aaa57ac39 -r 40e3c3be6bca src/HOL/Tools/Sledgehammer/MaSh/src/argparse.py
--- 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>.
diff -r 355aaa57ac39 -r 40e3c3be6bca src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py
--- 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
 
diff -r 355aaa57ac39 -r 40e3c3be6bca src/HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py
--- 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
 
diff -r 355aaa57ac39 -r 40e3c3be6bca src/HOL/Tools/Sledgehammer/MaSh/src/mash.py
--- 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
 
diff -r 355aaa57ac39 -r 40e3c3be6bca src/HOL/Tools/Sledgehammer/MaSh/src/naiveBayes.py
--- 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):
diff -r 355aaa57ac39 -r 40e3c3be6bca src/HOL/Tools/Sledgehammer/MaSh/src/predefined.py
--- 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
 
diff -r 355aaa57ac39 -r 40e3c3be6bca src/HOL/Tools/Sledgehammer/MaSh/src/readData.py
--- 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.
 
diff -r 355aaa57ac39 -r 40e3c3be6bca src/HOL/Tools/Sledgehammer/MaSh/src/snow.py
--- 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
diff -r 355aaa57ac39 -r 40e3c3be6bca src/HOL/Tools/Sledgehammer/MaSh/src/stats.py
--- 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