equal
deleted
inserted
replaced
165 (K (rewrite_goals_tac ac |
165 (K (rewrite_goals_tac ac |
166 THEN rtac Drule.reflexive_thm 1)) |
166 THEN rtac Drule.reflexive_thm 1)) |
167 end |
167 end |
168 |
168 |
169 (* instance for unions *) |
169 (* instance for unions *) |
170 fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Un} |
170 fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Set.union} |
171 (map (fn t => t RS eq_reflection) (@{thms "Un_ac"} @ |
171 (map (fn t => t RS eq_reflection) (@{thms Un_ac} @ |
172 @{thms "Un_empty_right"} @ |
172 @{thms Un_empty_right} @ |
173 @{thms "Un_empty_left"})) t |
173 @{thms Un_empty_left})) t |
174 |
174 |
175 |
175 |
176 end |
176 end |