equal
deleted
inserted
replaced
65 Have of rich_sequent | |
65 Have of rich_sequent | |
66 Cases of (clause * direct_inference list) list |
66 Cases of (clause * direct_inference list) list |
67 |
67 |
68 type direct_proof = direct_inference list |
68 type direct_proof = direct_inference list |
69 |
69 |
70 fun atom_eq p = (Atom.ord p = EQUAL) |
70 val atom_eq = is_equal o Atom.ord |
71 fun clause_eq (c, d) = (length c = length d andalso forall atom_eq (c ~~ d)) |
71 val clause_ord = dict_ord Atom.ord |
72 fun direct_sequent_eq ((gamma, c), (delta, d)) = |
72 val clause_eq = is_equal o clause_ord |
73 clause_eq (gamma, delta) andalso clause_eq (c, d) |
73 val direct_sequent_ord = prod_ord clause_ord clause_ord |
|
74 val direct_sequent_eq = is_equal o direct_sequent_ord |
74 |
75 |
75 fun make_refute_graph bot infers = |
76 fun make_refute_graph bot infers = |
76 let |
77 let |
77 fun add_edge to from = |
78 fun add_edge to from = |
78 Atom_Graph.default_node (from, ()) |
79 Atom_Graph.default_node (from, ()) |