author | blanchet |
Thu, 17 Jan 2013 23:53:55 +0100 | |
changeset 50966 | b85cb3049df9 |
parent 50965 | 7a7d1418301e |
child 50967 | 00d87ade2294 |
--- a/src/HOL/TPTP/MaSh_Export.thy Thu Jan 17 23:29:22 2013 +0100 +++ b/src/HOL/TPTP/MaSh_Export.thy Thu Jan 17 23:53:55 2013 +0100 @@ -105,4 +105,12 @@ () *} +ML {* +if do_it then + generate_mesh_suggestions max_suggestions (prefix ^ "mash_prover_suggestions") + (prefix ^ "mepo_suggestions") (prefix ^ "mesh_prover_suggestions") +else + () +*} + end