equal
deleted
inserted
replaced
189 (**********************************************************************) |
189 (**********************************************************************) |
190 |
190 |
191 fun spass_reconstruct_tac proofextract goalstring toParent ppid sg_num |
191 fun spass_reconstruct_tac proofextract goalstring toParent ppid sg_num |
192 clause_arr = |
192 clause_arr = |
193 SELECT_GOAL |
193 SELECT_GOAL |
194 (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, |
194 (EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac, |
195 METAHYPS(fn negs => |
195 METAHYPS(fn negs => |
196 Recon_Transfer.spass_reconstruct proofextract goalstring toParent ppid negs clause_arr)]) sg_num; |
196 Recon_Transfer.spass_reconstruct proofextract goalstring toParent ppid negs clause_arr)]) sg_num; |
197 |
197 |
198 |
198 |
199 fun transferSpassInput (fromChild, toParent, ppid, goalstring, |
199 fun transferSpassInput (fromChild, toParent, ppid, goalstring, |