equal
deleted
inserted
replaced
164 (* lemmas about simplifying id *) |
164 (* lemmas about simplifying id *) |
165 lemmas [id_simps] = |
165 lemmas [id_simps] = |
166 fun_map_id[THEN eq_reflection] |
166 fun_map_id[THEN eq_reflection] |
167 id_apply[THEN eq_reflection] |
167 id_apply[THEN eq_reflection] |
168 id_def[THEN eq_reflection, symmetric] |
168 id_def[THEN eq_reflection, symmetric] |
|
169 id_o[THEN eq_reflection] |
|
170 o_id[THEN eq_reflection] |
|
171 |
169 |
172 |
170 section {* Methods / Interface *} |
173 section {* Methods / Interface *} |
171 |
174 |
172 ML {* |
175 ML {* |
173 fun mk_method1 tac thm ctxt = |
176 fun mk_method1 tac thm ctxt = |