equal
deleted
inserted
replaced
273 then show "finite (range (tag_str_ALT A B))" |
273 then show "finite (range (tag_str_ALT A B))" |
274 unfolding tag_str_ALT_def quotient_def |
274 unfolding tag_str_ALT_def quotient_def |
275 by (rule rev_finite_subset) (auto) |
275 by (rule rev_finite_subset) (auto) |
276 next |
276 next |
277 show "\<And>x y. tag_str_ALT A B x = tag_str_ALT A B y \<Longrightarrow> x \<approx>(A \<union> B) y" |
277 show "\<And>x y. tag_str_ALT A B x = tag_str_ALT A B y \<Longrightarrow> x \<approx>(A \<union> B) y" |
278 unfolding tag_str_ALT_def |
278 unfolding tag_str_ALT_def |
279 unfolding str_eq_def |
279 unfolding str_eq_def |
280 unfolding str_eq_rel_def |
280 unfolding str_eq_rel_def |
281 by auto |
281 by auto |
282 qed |
282 qed |
283 |
283 |