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 = |
170 fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Un} |
171 regroup_conv (@{const_name Set.empty}) |
171 (map (fn t => t RS eq_reflection) (@{thms "Un_ac"} @ |
172 @{const_name Un} |
172 @{thms "Un_empty_right"} @ |
173 (map (fn t => t RS eq_reflection) (@{thms "Un_ac"} @ |
173 @{thms "Un_empty_left"})) t |
174 @{thms "Un_empty_right"} @ |
|
175 @{thms "Un_empty_left"})) t |
|
176 |
174 |
177 |
175 |
178 end |
176 end |