--- a/src/HOL/TPTP/ATP_Theory_Export.thy Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy Thu May 26 17:51:22 2016 +0200
@@ -2,7 +2,7 @@
Author: Jasmin Blanchette, TU Muenchen
*)
-section {* ATP Theory Exporter *}
+section \<open>ATP Theory Exporter\<close>
theory ATP_Theory_Export
imports Complex_Main
@@ -10,61 +10,61 @@
ML_file "atp_theory_export.ML"
-ML {*
+ML \<open>
open ATP_Problem
open ATP_Theory_Export
-*}
+\<close>
-ML {*
+ML \<open>
val do_it = false (* switch to "true" to generate the files *)
val ctxt = @{context}
val thy = @{theory Complex_Main}
val infer_policy = (* Unchecked_Inferences *) No_Inferences
-*}
+\<close>
-ML {*
+ML \<open>
if do_it then
"/tmp/isa_filter"
|> generate_casc_lbt_isa_files_for_theory ctxt thy (THF (Polymorphic, THF_Without_Choice))
infer_policy "poly_native_higher"
else
()
-*}
+\<close>
-ML {*
+ML \<open>
if do_it then
"/tmp/axs_tc_native.dfg"
|> generate_atp_inference_file_for_theory ctxt thy (DFG Polymorphic)
infer_policy "tc_native"
else
()
-*}
+\<close>
-ML {*
+ML \<open>
if do_it then
"/tmp/infs_poly_guards_query_query.tptp"
|> generate_atp_inference_file_for_theory ctxt thy FOF infer_policy
"poly_guards??"
else
()
-*}
+\<close>
-ML {*
+ML \<open>
if do_it then
"/tmp/infs_poly_tags_query_query.tptp"
|> generate_atp_inference_file_for_theory ctxt thy FOF infer_policy
"poly_tags??"
else
()
-*}
+\<close>
-ML {*
+ML \<open>
if do_it then
"/tmp/casc_ltb_isa"
|> generate_casc_lbt_isa_files_for_theory ctxt thy FOF infer_policy
"poly_tags??"
else
()
-*}
+\<close>
end