changeset 48235 | 40655464a93b |
parent 48234 | 06216c789ac9 |
child 48236 | e174ecc4f5a4 |
--- a/src/HOL/TPTP/MaSh_Import.thy Tue Jul 10 23:36:03 2012 +0200 +++ b/src/HOL/TPTP/MaSh_Import.thy Tue Jul 10 23:36:03 2012 +0200 @@ -9,4 +9,18 @@ uses "mash_import.ML" begin +ML {* +open MaSh_Import +*} + +ML {* +val do_it = true (* switch to "true" to generate the files *); +val thy = @{theory List} +*} + +ML {* +if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions2" +else () +*} + end