# HG changeset patch
# User blanchet
# Date 1365513554 -7200
# Node ID 3e09226c33782d8978be5c7426a9208d009d1109
# Parent  25acf689a53efc22d77b976a5bfd49d28b720585
reverted accidental changes to theory file + updated wrt ML file

diff -r 25acf689a53e -r 3e09226c3378 src/HOL/TPTP/ATP_Theory_Export.thy
--- a/src/HOL/TPTP/ATP_Theory_Export.thy	Tue Apr 09 15:19:14 2013 +0200
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy	Tue Apr 09 15:19:14 2013 +0200
@@ -5,7 +5,7 @@
 header {* ATP Theory Exporter *}
 
 theory ATP_Theory_Export
-imports "~~/src/HOL/Sledgehammer2d"(*###*) Complex_Main
+imports Complex_Main
 begin
 
 ML_file "atp_theory_export.ML"
@@ -16,25 +16,46 @@
 *}
 
 ML {*
-val do_it = true (* ### *)
-val thy = @{theory Orderings}
+val do_it = false (* switch to "true" to generate the files *)
 val ctxt = @{context}
+val thy = @{theory List}
+val infer_policy = Unchecked_Inferences
+*}
+
+ML {*
+if do_it then
+  "/tmp/axs_tc_native.dfg"
+  |> generate_atp_inference_file_for_theory ctxt thy (DFG Polymorphic)
+         infer_policy "tc_native"
+else
+  ()
 *}
 
 ML {*
-"/tmp/casc_ltb_isa"
-|> generate_casc_lbt_isa_files_for_theory ctxt thy FOF Unchecked_Inferences
-        "poly_tags??"
+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
+  ()
 *}
 
-
-
+ML {*
+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
+  ()
+*}
 
 ML {*
-"/tmp/orderings.tptp"
-|> generate_atp_inference_file_for_theory ctxt thy FOF Unchecked_Inferences
-       "poly_tags??"
+if do_it then
+  "/tmp/casc_ltb_isa"
+  |> generate_casc_lbt_isa_files_for_theory ctxt thy FOF infer_policy
+         "poly_tags??"
+else
+  ()
 *}
 
-
 end