| changeset 939 | ce774af6b964 |
| parent 930 | 68c1f378a70a |
| child 1068 | 62e54830590f |
| 938:0ff855a6ffb7 | 939:ce774af6b964 |
|---|---|
110 |
110 |
111 text {* Lemmas about simplifying id's. *} |
111 text {* Lemmas about simplifying id's. *} |
112 lemmas [id_simps] = |
112 lemmas [id_simps] = |
113 id_def[symmetric] |
113 id_def[symmetric] |
114 fun_map_id |
114 fun_map_id |
115 id_apply[THEN eq_reflection] |
115 id_apply |
116 id_o |
116 id_o |
117 o_id |
117 o_id |
118 eq_comp_r |
118 eq_comp_r |
119 |
119 |
120 text {* Translation functions for the lifting process. *} |
120 text {* Translation functions for the lifting process. *} |