--- a/src/HOL/TPTP/MaSh_Export.thy Thu Jan 17 18:53:13 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy Thu Jan 17 19:20:56 2013 +0100
@@ -29,6 +29,8 @@
val thys = [@{theory List}]
val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
val prover = hd provers
+val range = (1, NONE)
+val step = 1
val max_suggestions = 1536
val dir = "List"
val prefix = "/tmp/" ^ dir ^ "/"
@@ -65,15 +67,16 @@
ML {*
if do_it then
- generate_isar_commands @{context} prover thys (prefix ^ "mash_commands")
+ generate_isar_commands @{context} prover (range, step) thys
+ (prefix ^ "mash_commands")
else
()
*}
ML {*
if do_it then
- generate_mepo_suggestions @{context} params (1, NONE) thys max_suggestions
- (prefix ^ "mepo_suggestions")
+ generate_mepo_suggestions @{context} params (range, step) thys
+ max_suggestions (prefix ^ "mepo_suggestions")
else
()
*}
@@ -88,7 +91,7 @@
ML {*
if do_it then
- generate_prover_dependencies @{context} params (1, NONE) thys false
+ generate_prover_dependencies @{context} params range thys false
(prefix ^ "mash_prover_dependencies")
else
()
@@ -96,7 +99,7 @@
ML {*
if do_it then
- generate_prover_commands @{context} params (1, NONE) thys
+ generate_prover_commands @{context} params (range, step) thys
(prefix ^ "mash_prover_commands")
else
()