equal
deleted
inserted
replaced
109 lemmas [quot_equiv] = identity_equivp |
109 lemmas [quot_equiv] = identity_equivp |
110 |
110 |
111 |
111 |
112 text {* Lemmas about simplifying id's. *} |
112 text {* Lemmas about simplifying id's. *} |
113 lemmas [id_simps] = |
113 lemmas [id_simps] = |
114 id_def[symmetric, THEN eq_reflection] |
114 id_def[symmetric] |
115 fun_map_id[THEN eq_reflection] |
115 fun_map_id[THEN eq_reflection] |
116 id_apply[THEN eq_reflection] |
116 id_apply[THEN eq_reflection] |
117 id_o[THEN eq_reflection] |
117 id_o[THEN eq_reflection] |
118 o_id[THEN eq_reflection] |
118 o_id[THEN eq_reflection] |
119 eq_comp_r |
119 eq_comp_r |