diff -r 50e00ee405f8 -r 06216c789ac9 src/HOL/TPTP/MaSh_Export.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/MaSh_Export.thy	Tue Jul 10 23:36:03 2012 +0200
@@ -0,0 +1,54 @@
+(*  Title:      HOL/TPTP/MaSh_Export.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+*)
+
+header {* MaSh Exporter *}
+
+theory MaSh_Export
+imports ATP_Theory_Export
+uses "mash_export.ML"
+begin
+
+ML {*
+open MaSh_Export
+*}
+
+ML {*
+val do_it = false; (* switch to "true" to generate the files *)
+val thy = @{theory List};
+val ctxt = @{context}
+*}
+
+ML {*
+if do_it then
+  "/tmp/mash_sample_problem.out"
+  |> generate_mash_problem_file_for_theory thy
+else
+  ()
+*}
+
+ML {*
+if do_it then
+  "/tmp/mash_features.out"
+  |> generate_mash_feature_file_for_theory thy false
+else
+  ()
+*}
+
+ML {*
+if do_it then
+  "/tmp/mash_accessibility.out"
+  |> generate_mash_accessibility_file_for_theory thy false
+else
+  ()
+*}
+
+ML {*
+if do_it then
+  "/tmp/mash_dependencies.out"
+  |> generate_mash_dependency_file_for_theory thy false
+else
+   ()
+*}
+
+end