| author | blanchet |
| Wed, 11 Jul 2012 21:43:19 +0200 | |
| changeset 49265 | 1065c307fafe |
| parent 49260 | 854a47677335 |
| child 49266 | 6cdcfbddc077 |
| 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@49251 | 12 |
declare [[sledgehammer_instantiate_inducts]] |
| blanchet@49251 | 13 |
|
| blanchet@49250 | 14 |
ML {*
|
| blanchet@49250 | 15 |
open MaSh_Import |
| blanchet@49250 | 16 |
*} |
| blanchet@49250 | 17 |
|
| blanchet@49250 | 18 |
ML {*
|
| blanchet@49265 | 19 |
val do_it = true (* switch to "true" to generate the files *); |
| blanchet@49260 | 20 |
val thy = @{theory List}
|
| blanchet@49250 | 21 |
*} |
| blanchet@49250 | 22 |
|
| blanchet@49250 | 23 |
ML {*
|
| blanchet@49265 | 24 |
if do_it then |
| blanchet@49265 | 25 |
import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions_list"
|
| blanchet@49265 | 26 |
else |
| blanchet@49265 | 27 |
() |
| blanchet@49250 | 28 |
*} |
| blanchet@49250 | 29 |
|
| blanchet@49249 | 30 |
end |