--- a/src/HOL/TPTP/MaSh_Export_Base.thy Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/TPTP/MaSh_Export_Base.thy Thu May 26 17:51:22 2016 +0200
@@ -2,7 +2,7 @@
Author: Jasmin Blanchette, TU Muenchen
*)
-section {* MaSh Exporter Base *}
+section \<open>MaSh Exporter Base\<close>
theory MaSh_Export_Base
imports Main
@@ -19,15 +19,15 @@
hide_fact (open) HOL.ext
-ML {*
+ML \<open>
Multithreading.max_threads ()
-*}
+\<close>
-ML {*
+ML \<open>
open MaSh_Export
-*}
+\<close>
-ML {*
+ML \<open>
val do_it = false (* switch to "true" to generate the files *)
val thys = [@{theory List}]
val params as {provers, ...} = Sledgehammer_Commands.default_params @{theory} []
@@ -37,6 +37,6 @@
val max_suggestions = 1024
val dir = "List"
val prefix = "/tmp/" ^ dir ^ "/"
-*}
+\<close>
end