equal
deleted
inserted
replaced
66 |
66 |
67 type direct_proof = direct_inference list |
67 type direct_proof = direct_inference list |
68 |
68 |
69 val atom_eq = is_equal o Atom.ord |
69 val atom_eq = is_equal o Atom.ord |
70 val clause_ord = dict_ord Atom.ord |
70 val clause_ord = dict_ord Atom.ord |
71 fun direct_sequent_ord seqp = prod_ord clause_ord clause_ord (pairself snd seqp) |
71 fun direct_sequent_ord seqp = prod_ord clause_ord clause_ord (apply2 snd seqp) |
72 fun direct_sequent_eq seqp = is_equal (direct_sequent_ord seqp) |
72 fun direct_sequent_eq seqp = is_equal (direct_sequent_ord seqp) |
73 |
73 |
74 fun make_refute_graph bot infers = |
74 fun make_refute_graph bot infers = |
75 let |
75 let |
76 fun add_edge to from = |
76 fun add_edge to from = |