diff -r 50e00ee405f8 -r 06216c789ac9 src/HOL/TPTP/mash_import.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/mash_import.ML	Tue Jul 10 23:36:03 2012 +0200
@@ -0,0 +1,15 @@
+(*  Title:      HOL/TPTP/mash_import.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2012
+
+Import proof suggestions from MaSh (Machine-learning for Sledgehammer) and
+evaluate them.
+*)
+
+signature MASH_IMPORT =
+sig
+end;
+
+structure MaSh_Import : MASH_IMPORT =
+struct
+end;