Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tuned renaming
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Tue, 20 Dec 2011 11:40:04 +0900
changeset 3079 a303ef51cd97
parent 3078 abf147627b4b
child 3080 9253984db291
Tuned renaming
Nominal/Ex/BetaCR.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Ex/BetaCR.thy	Mon Dec 19 16:39:20 2011 +0900
+++ b/Nominal/Ex/BetaCR.thy	Tue Dec 20 11:40:04 2011 +0900
@@ -243,7 +243,7 @@
 quotient_definition "QVar::name \<Rightarrow> qlam" is Var
 quotient_definition "QApp::qlam \<Rightarrow> qlam \<Rightarrow> qlam" is App
 quotient_definition QLam ("QLam [_]._")
-  where "QLam::name \<Rightarrow> qlam \<Rightarrow> qlam" is Beta.Lam
+  where "QLam::name \<Rightarrow> qlam \<Rightarrow> qlam" is BetaCR.Lam
 
 lemmas qlam_strong_induct = lam.strong_induct[quot_lifted]
 lemmas qlam_induct = lam.induct[quot_lifted]
nominal2