equal
deleted
inserted
replaced
90 by (case_tac p) (auto simp add: Quotient_abs_rep[OF q2]) |
90 by (case_tac p) (auto simp add: Quotient_abs_rep[OF q2]) |
91 |
91 |
92 lemma prod_fun_id[id_simps]: "prod_fun id id \<equiv> id" |
92 lemma prod_fun_id[id_simps]: "prod_fun id id \<equiv> id" |
93 by (rule eq_reflection) (simp add: prod_fun_def) |
93 by (rule eq_reflection) (simp add: prod_fun_def) |
94 |
94 |
|
95 lemma prod_rel_eq[id_simps]: "prod_rel op = op = \<equiv> op =" |
|
96 apply (rule eq_reflection) |
|
97 apply (rule ext)+ |
|
98 apply auto |
|
99 done |
|
100 |
95 section {* general setup for products *} |
101 section {* general setup for products *} |
96 |
102 |
97 declare [[map * = (prod_fun, prod_rel)]] |
103 declare [[map * = (prod_fun, prod_rel)]] |
98 |
104 |
99 lemmas [quot_thm] = prod_quotient |
105 lemmas [quot_thm] = prod_quotient |