changeset 46435 | e9c90516bc0d |
parent 46321 | 484dc68c8c89 |
child 48129 | 933d43c31689 |
--- a/src/HOL/TPTP/ATP_Theory_Export.thy Sun Feb 05 17:43:15 2012 +0100 +++ b/src/HOL/TPTP/ATP_Theory_Export.thy Mon Feb 06 23:01:01 2012 +0100 @@ -22,9 +22,9 @@ ML {* if do_it then - "/tmp/axs_mono_simple.dfg" + "/tmp/axs_mono_native.dfg" |> generate_tptp_inference_file_for_theory ctxt thy (DFG DFG_Sorted) - "mono_simple" + "mono_native" else () *}