author | blanchet |
Tue, 10 Jul 2012 23:36:03 +0200 | |
changeset 49250 | 40655464a93b |
parent 49249 | 06216c789ac9 |
child 49251 | e174ecc4f5a4 |
permissions | -rw-r--r-- |
blanchet@49249 | 1 |
(* Title: HOL/TPTP/MaSh_Import.thy |
blanchet@49249 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
blanchet@49249 | 3 |
*) |
blanchet@49249 | 4 |
|
blanchet@49249 | 5 |
header {* MaSh Importer *} |
blanchet@49249 | 6 |
|
blanchet@49249 | 7 |
theory MaSh_Import |
blanchet@49249 | 8 |
imports MaSh_Export |
blanchet@49249 | 9 |
uses "mash_import.ML" |
blanchet@49249 | 10 |
begin |
blanchet@49249 | 11 |
|
blanchet@49250 | 12 |
ML {* |
blanchet@49250 | 13 |
open MaSh_Import |
blanchet@49250 | 14 |
*} |
blanchet@49250 | 15 |
|
blanchet@49250 | 16 |
ML {* |
blanchet@49250 | 17 |
val do_it = true (* switch to "true" to generate the files *); |
blanchet@49250 | 18 |
val thy = @{theory List} |
blanchet@49250 | 19 |
*} |
blanchet@49250 | 20 |
|
blanchet@49250 | 21 |
ML {* |
blanchet@49250 | 22 |
if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions2" |
blanchet@49250 | 23 |
else () |
blanchet@49250 | 24 |
*} |
blanchet@49250 | 25 |
|
blanchet@49249 | 26 |
end |