equal
deleted
inserted
replaced
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_o[THEN eq_reflection] |
110 id_o[THEN eq_reflection] |
|
111 id_def[symmetric, THEN eq_reflection] |
111 o_id[THEN eq_reflection] |
112 o_id[THEN eq_reflection] |
112 eq_comp_r |
113 eq_comp_r |
113 |
114 |
114 (* The translation functions for the lifting process. *) |
115 (* The translation functions for the lifting process. *) |
115 use "quotient_term.ML" |
116 use "quotient_term.ML" |