equal
deleted
inserted
replaced
80 |
80 |
81 in |
81 in |
82 |
82 |
83 fun add_cong raw_thm congs = |
83 fun add_cong raw_thm congs = |
84 let val (c, thm) = prep_cong raw_thm |
84 let val (c, thm) = prep_cong raw_thm |
85 in overwrite_warn (congs, (c, thm)) ("Overwriting recdef congruence rule for " ^ quote c) end; |
85 in update_warn (op =) ("Overwriting recdef congruence rule for " ^ quote c) (c, thm) congs end; |
86 |
86 |
87 fun del_cong raw_thm congs = |
87 fun del_cong raw_thm congs = |
88 let |
88 let |
89 val (c, thm) = prep_cong raw_thm; |
89 val (c, thm) = prep_cong raw_thm; |
90 val (del, rest) = Library.partition (Library.equal c o fst) congs; |
90 val (del, rest) = Library.partition (Library.equal c o fst) congs; |