equal
deleted
inserted
replaced
73 |
73 |
74 fun nitpick_tptp_file thy timeout file_name = |
74 fun nitpick_tptp_file thy timeout file_name = |
75 let |
75 let |
76 val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name |
76 val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name |
77 val thy = Proof_Context.theory_of ctxt |
77 val thy = Proof_Context.theory_of ctxt |
78 val defs = defs |> map (ATP_Util.abs_extensionalize_term ctxt |
78 val (defs, pseudo_defs) = |
79 #> aptrueprop (open_form I)) |
79 defs |> map (ATP_Util.abs_extensionalize_term ctxt |
|
80 #> aptrueprop (open_form I)) |
|
81 |> List.partition (ATP_Util.is_legitimate_tptp_def |
|
82 o perhaps (try HOLogic.dest_Trueprop) |
|
83 o ATP_Util.unextensionalize_def) |
|
84 val nondefs = pseudo_defs @ nondefs |
80 val state = Proof.init ctxt |
85 val state = Proof.init ctxt |
81 val params = |
86 val params = |
82 [("card", "1\<emdash>100"), |
87 [("card", "1\<emdash>100"), |
83 ("box", "false"), |
88 ("box", "false"), |
84 ("max_threads", "1"), |
89 ("max_threads", "1"), |