equal
deleted
inserted
replaced
241 (erule equ_trans, assumption) |
241 (erule equ_trans, assumption) |
242 |
242 |
243 quotient_definition "QVar::name \<Rightarrow> qlam" is Var |
243 quotient_definition "QVar::name \<Rightarrow> qlam" is Var |
244 quotient_definition "QApp::qlam \<Rightarrow> qlam \<Rightarrow> qlam" is App |
244 quotient_definition "QApp::qlam \<Rightarrow> qlam \<Rightarrow> qlam" is App |
245 quotient_definition QLam ("QLam [_]._") |
245 quotient_definition QLam ("QLam [_]._") |
246 where "QLam::name \<Rightarrow> qlam \<Rightarrow> qlam" is Beta.Lam |
246 where "QLam::name \<Rightarrow> qlam \<Rightarrow> qlam" is BetaCR.Lam |
247 |
247 |
248 lemmas qlam_strong_induct = lam.strong_induct[quot_lifted] |
248 lemmas qlam_strong_induct = lam.strong_induct[quot_lifted] |
249 lemmas qlam_induct = lam.induct[quot_lifted] |
249 lemmas qlam_induct = lam.induct[quot_lifted] |
250 |
250 |
251 instantiation qlam :: pt |
251 instantiation qlam :: pt |