equal
deleted
inserted
replaced
209 |
209 |
210 lemmas [id_simps] = |
210 lemmas [id_simps] = |
211 fun_map_id[THEN eq_reflection] |
211 fun_map_id[THEN eq_reflection] |
212 id_apply[THEN eq_reflection] |
212 id_apply[THEN eq_reflection] |
213 id_def[THEN eq_reflection,symmetric] |
213 id_def[THEN eq_reflection,symmetric] |
214 |
|
215 section {* Debugging infrastructure for testing tactics *} |
|
216 |
|
217 ML {* |
|
218 fun my_print_tac ctxt s i thm = |
|
219 let |
|
220 val prem_str = nth (prems_of thm) (i - 1) |
|
221 |> Syntax.string_of_term ctxt |
|
222 handle Subscript => "no subgoal" |
|
223 val _ = tracing (s ^ "\n" ^ prem_str) |
|
224 in |
|
225 Seq.single thm |
|
226 end *} |
|
227 |
214 |
228 section {* Matching of Terms and Types *} |
215 section {* Matching of Terms and Types *} |
229 |
216 |
230 ML {* |
217 ML {* |
231 fun struct_match_typ (ty, ty') = |
218 fun struct_match_typ (ty, ty') = |