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