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 val clause_eq = is_equal o clause_ord |
|
72 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 (pairself snd seqp) |
73 fun direct_sequent_eq seqp = is_equal (direct_sequent_ord seqp) |
72 fun direct_sequent_eq seqp = is_equal (direct_sequent_ord seqp) |
74 |
73 |
75 fun make_refute_graph bot infers = |
74 fun make_refute_graph bot infers = |
76 let |
75 let |