author | blanchet |
Tue, 10 Jul 2012 23:36:03 +0200 | |
changeset 48235 | 40655464a93b |
parent 48234 | 06216c789ac9 |
child 48236 | e174ecc4f5a4 |
permissions | -rw-r--r-- |
(* Title: HOL/TPTP/MaSh_Import.thy Author: Jasmin Blanchette, TU Muenchen *) header {* MaSh Importer *} theory MaSh_Import imports MaSh_Export 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