(*  Title:      HOL/TPTP/MaSh_Export.thy

     Author:     Jasmin Blanchette, TU Muenchen

 *)

 header {* MaSh Exporter *}

 theory MaSh_Export

 imports ATP_Theory_Export

 uses "mash_export.ML"

 begin

 ML {*

 open MaSh_Export

 *}

 ML {*

 val do_it = false; (* switch to "true" to generate the files *)

 val thy = @{theory List};

 val ctxt = @{context}

 *}

 ML {*

 if do_it then

   "/tmp/mash_sample_problem.out"

   |> generate_mash_problem_file_for_theory thy

 else

   ()

 *}

 ML {*

 if do_it then

   "/tmp/mash_features.out"

   |> generate_mash_feature_file_for_theory thy false

 else

   ()

 *}

 ML {*

 if do_it then

   "/tmp/mash_accessibility.out"

   |> generate_mash_accessibility_file_for_theory thy false

 else

   ()

 *}

 ML {*

 if do_it then

   "/tmp/mash_dependencies.out"

   |> generate_mash_dependency_file_for_theory thy false

 else

    ()

 *}

 end