| author | blanchet |
| Wed, 11 Jul 2012 21:43:19 +0200 | |
| changeset 49265 | 1065c307fafe |
| parent 49260 | 854a47677335 |
| child 49266 | 6cdcfbddc077 |
| permissions | -rw-r--r-- |
1 (* Title: HOL/TPTP/MaSh_Import.thy
2 Author: Jasmin Blanchette, TU Muenchen
3 *)
5 header {* MaSh Importer *}
7 theory MaSh_Import
8 imports MaSh_Export
9 uses "mash_import.ML"
10 begin
12 declare [[sledgehammer_instantiate_inducts]]
14 ML {*
15 open MaSh_Import
16 *}
18 ML {*
19 val do_it = true (* switch to "true" to generate the files *);
20 val thy = @{theory List}
21 *}
23 ML {*
24 if do_it then
25 import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions_list"
26 else
27 ()
28 *}
30 end