1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Tue Jul 10 23:36:03 2012 +0200
     1.3 @@ -0,0 +1,54 @@
     1.4 +(*  Title:      HOL/TPTP/MaSh_Export.thy
     1.5 +    Author:     Jasmin Blanchette, TU Muenchen
     1.6 +*)
     1.7 +
     1.8 +header {* MaSh Exporter *}
     1.9 +
    1.10 +theory MaSh_Export
    1.11 +imports ATP_Theory_Export
    1.12 +uses "mash_export.ML"
    1.13 +begin
    1.14 +
    1.15 +ML {*
    1.16 +open MaSh_Export
    1.17 +*}
    1.18 +
    1.19 +ML {*
    1.20 +val do_it = false; (* switch to "true" to generate the files *)
    1.21 +val thy = @{theory List};
    1.22 +val ctxt = @{context}
    1.23 +*}
    1.24 +
    1.25 +ML {*
    1.26 +if do_it then
    1.27 +  "/tmp/mash_sample_problem.out"
    1.28 +  |> generate_mash_problem_file_for_theory thy
    1.29 +else
    1.30 +  ()
    1.31 +*}
    1.32 +
    1.33 +ML {*
    1.34 +if do_it then
    1.35 +  "/tmp/mash_features.out"
    1.36 +  |> generate_mash_feature_file_for_theory thy false
    1.37 +else
    1.38 +  ()
    1.39 +*}
    1.40 +
    1.41 +ML {*
    1.42 +if do_it then
    1.43 +  "/tmp/mash_accessibility.out"
    1.44 +  |> generate_mash_accessibility_file_for_theory thy false
    1.45 +else
    1.46 +  ()
    1.47 +*}
    1.48 +
    1.49 +ML {*
    1.50 +if do_it then
    1.51 +  "/tmp/mash_dependencies.out"
    1.52 +  |> generate_mash_dependency_file_for_theory thy false
    1.53 +else
    1.54 +   ()
    1.55 +*}
    1.56 +
    1.57 +end