equal
deleted
inserted
replaced
105 |
105 |
106 (* Lemmas about simplifying id's. *) |
106 (* Lemmas about simplifying id's. *) |
107 lemmas [id_simps] = |
107 lemmas [id_simps] = |
108 fun_map_id[THEN eq_reflection] |
108 fun_map_id[THEN eq_reflection] |
109 id_apply[THEN eq_reflection] |
109 id_apply[THEN eq_reflection] |
110 (*id_def[THEN eq_reflection, symmetric]*) |
|
111 id_o[THEN eq_reflection] |
110 id_o[THEN eq_reflection] |
112 o_id[THEN eq_reflection] |
111 o_id[THEN eq_reflection] |
113 eq_comp_r |
112 eq_comp_r |
114 |
113 |
115 (* The translation functions for the lifting process. *) |
114 (* The translation functions for the lifting process. *) |