equal
deleted
inserted
replaced
102 (*** theorem tags ***) |
102 (*** theorem tags ***) |
103 |
103 |
104 (* add / delete tags *) |
104 (* add / delete tags *) |
105 |
105 |
106 fun map_tags f thm = |
106 fun map_tags f thm = |
107 Thm.put_name_tags (Thm.name_of_thm thm, f (#2 (Thm.get_name_tags thm))) thm; |
107 let val (name, tags) = Thm.get_name_tags thm |
|
108 in Thm.put_name_tags (name, f tags) thm end; |
108 |
109 |
109 fun tag_rule tg = map_tags (fn tgs => if member (op =) tgs tg then tgs else tgs @ [tg]); |
110 fun tag_rule tg = map_tags (fn tgs => if member (op =) tgs tg then tgs else tgs @ [tg]); |
110 fun untag_rule s = map_tags (filter_out (fn (s', _) => s = s')); |
111 fun untag_rule s = map_tags (filter_out (fn (s', _) => s = s')); |
111 |
112 |
112 fun tag tg x = Thm.rule_attribute (K (tag_rule tg)) x; |
113 fun tag tg x = Thm.rule_attribute (K (tag_rule tg)) x; |