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.
Fixed rbv6, when translating to OTT.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 10 Feb 2010 11:31:43 +0100
changeset 1117 8948319b190e
parent 1116 3acc7d25627a
child 1118 3e405c2fbe90
Fixed rbv6, when translating to OTT.
Quot/Nominal/Terms.thy file | annotate | diff | comparison | revisions 
--- a/Quot/Nominal/Terms.thy	Wed Feb 10 11:27:49 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 10 11:31:43 2010 +0100
@@ -936,7 +936,7 @@
   rbv6
 where
   "rbv6 (rVr6 n) = {}"
-| "rbv6 (rLm6 n t) = {atom n}"
+| "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t"
 | "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r"
 
 primrec
nominal2