equal
deleted
inserted
replaced
213 |
213 |
214 fun add_fact _ facts_offset fact_names (Inference (name, _, [])) = |
214 fun add_fact _ facts_offset fact_names (Inference (name, _, [])) = |
215 union (op =) (resolve_fact facts_offset fact_names name) |
215 union (op =) (resolve_fact facts_offset fact_names name) |
216 | add_fact ctxt _ _ (Inference (_, _, deps)) = |
216 | add_fact ctxt _ _ (Inference (_, _, deps)) = |
217 if AList.defined (op =) deps leo2_ext then |
217 if AList.defined (op =) deps leo2_ext then |
218 insert (op =) (ext_name ctxt, General (* or Chained... *)) |
218 insert (op =) (ext_name ctxt, Extensionality) |
219 else |
219 else |
220 I |
220 I |
221 | add_fact _ _ _ _ = I |
221 | add_fact _ _ _ _ = I |
222 |
222 |
223 fun used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof = |
223 fun used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof = |