equal
deleted
inserted
replaced
54 setup {* |
54 setup {* |
55 Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #> |
55 Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #> |
56 Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #> |
56 Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #> |
57 Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2)) |
57 Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2)) |
58 *} |
58 *} |
|
59 |
|
60 lemma insert_preserve2: |
|
61 shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) = |
|
62 (id ---> rep_fset ---> abs_fset) op #" |
|
63 by (simp add: fun_eq_iff abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset]) |
59 |
64 |
60 (*>*) |
65 (*>*) |
61 |
66 |
62 |
67 |
63 section {* Introduction *} |
68 section {* Introduction *} |