equal
deleted
inserted
replaced
496 exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false) |
496 exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false) |
497 |
497 |
498 val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg" |
498 val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg" |
499 |
499 |
500 fun add_fact ctxt facts ((_, ss), _, _, rule, deps) = |
500 fun add_fact ctxt facts ((_, ss), _, _, rule, deps) = |
501 (if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule, satallax_core_rule] rule then |
501 (if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule] rule then |
502 insert (op =) (short_thm_name ctxt ext, (Global, General)) |
502 insert (op =) (short_thm_name ctxt ext, (Global, General)) |
503 else |
503 else |
504 I) |
504 I) |
505 #> (if null deps then union (op =) (resolve_facts facts ss) else I) |
505 #> (if null deps then union (op =) (resolve_facts facts ss) else I) |
506 |
506 |