equal
deleted
inserted
replaced
258 assumes a: "alpha_lam_raw t1 t2" |
258 assumes a: "alpha_lam_raw t1 t2" |
259 shows "alpha_lam_raw (p \<bullet> t1) (p \<bullet> t2)" |
259 shows "alpha_lam_raw (p \<bullet> t1) (p \<bullet> t2)" |
260 using a |
260 using a |
261 apply(induct) |
261 apply(induct) |
262 apply(tactic {* my_tac @{context} @{thms alpha_lam_raw.intros} 1 *}) |
262 apply(tactic {* my_tac @{context} @{thms alpha_lam_raw.intros} 1 *}) |
263 apply(tactic {* my_tac @{context} @{thms alpha_lam_raw.intros} 1 *}) |
|
264 apply(perm_strict_simp) |
|
265 apply(rule alpha_lam_raw.intros) |
|
266 apply(simp) |
|
267 apply(perm_strict_simp) |
|
268 apply(rule alpha_lam_raw.intros) |
|
269 apply(simp add: alphas) |
|
270 apply(rule_tac p="- p" in permute_boolE) |
|
271 apply(perm_simp permute_minus_cancel(2)) |
|
272 oops |
263 oops |
273 |
264 |
274 thm alpha_lam_raw.intros[no_vars] |
265 thm alpha_lam_raw.intros[no_vars] |
275 |
266 |
276 inductive |
267 inductive |