equal
deleted
inserted
replaced
460 "match_Var :: lam \<Rightarrow> name option" |
460 "match_Var :: lam \<Rightarrow> name option" |
461 is match_Var_raw |
461 is match_Var_raw |
462 |
462 |
463 lemma [quot_respect]: "(alpha_lam_raw ===> op =) match_Var_raw match_Var_raw" |
463 lemma [quot_respect]: "(alpha_lam_raw ===> op =) match_Var_raw match_Var_raw" |
464 apply rule |
464 apply rule |
465 apply (induct_tac a b rule: alpha_lam_raw.induct) |
465 apply (induct_tac x y rule: alpha_lam_raw.induct) |
466 apply simp_all |
466 apply simp_all |
467 done |
467 done |
468 |
468 |
469 lemmas match_Var_simps = match_Var_raw.simps[quot_lifted] |
469 lemmas match_Var_simps = match_Var_raw.simps[quot_lifted] |
470 |
470 |