equal
deleted
inserted
replaced
36 val empty = Net.empty |
36 val empty = Net.empty |
37 val extend = I |
37 val extend = I |
38 val merge = Net.merge eq |
38 val merge = Net.merge eq |
39 ) |
39 ) |
40 |
40 |
41 val prep = |
41 val prep = `Thm.prop_of o rewrite_rule [Z3_Proof_Literals.rewrite_true] |
42 `Thm.prop_of o Simplifier.rewrite_rule [Z3_Proof_Literals.rewrite_true] |
|
43 |
42 |
44 fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net |
43 fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net |
45 fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net |
44 fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net |
46 |
45 |
47 val add = Thm.declaration_attribute (Z3_Rules.map o ins) |
46 val add = Thm.declaration_attribute (Z3_Rules.map o ins) |