equal
deleted
inserted
replaced
57 apply(simp add: Quotient_rep_reflp[OF q]) |
57 apply(simp add: Quotient_rep_reflp[OF q]) |
58 apply(rule allI)+ |
58 apply(rule allI)+ |
59 apply(rule list_rel_rel[OF q]) |
59 apply(rule list_rel_rel[OF q]) |
60 done |
60 done |
61 |
61 |
62 lemma map_id: "map id \<equiv> id" |
62 lemma map_id[id_simps]: "map id \<equiv> id" |
63 apply (rule eq_reflection) |
63 apply (rule eq_reflection) |
64 apply (rule ext) |
64 apply (rule ext) |
65 apply (rule_tac list="x" in list.induct) |
65 apply (rule_tac list="x" in list.induct) |
66 apply (simp_all) |
66 apply (simp_all) |
67 done |
67 done |