--- a/src/HOL/TPTP/MaSh_Export.thy Thu Jan 10 23:02:58 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy Thu Jan 10 23:34:19 2013 +0100
@@ -29,6 +29,7 @@
val thys = [@{theory List}]
val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
val prover = hd provers
+val max_suggestions = 1024
val dir = "List"
val prefix = "/tmp/" ^ dir ^ "/"
*}
@@ -70,9 +71,17 @@
*}
ML {*
+if true orelse do_it then
+ generate_mepo_suggestions @{context} params thys max_suggestions
+ (prefix ^ "mepo_suggestions")
+else
+ ()
+*}
+
+ML {*
if do_it then
- generate_mepo_suggestions @{context} params thys 1024
- (prefix ^ "mash_mepo_suggestions")
+ generate_mesh_suggestions max_suggestions (prefix ^ "mash_suggestions")
+ (prefix ^ "mepo_suggestions") (prefix ^ "mesh_suggestions")
else
()
*}