equal
deleted
inserted
replaced
942 primrec |
942 primrec |
943 rfv_trm6 |
943 rfv_trm6 |
944 where |
944 where |
945 "rfv_trm6 (rVr6 n) = {atom n}" |
945 "rfv_trm6 (rVr6 n) = {atom n}" |
946 | "rfv_trm6 (rLm6 n t) = (rfv_trm6 t) - {atom n}" |
946 | "rfv_trm6 (rLm6 n t) = (rfv_trm6 t) - {atom n}" |
947 | "rfv_trm6 (rLt6 l r) = (rfv_trm6 r - rbv6 l) \<union> rfv_trm6 r" |
947 | "rfv_trm6 (rLt6 l r) = (rfv_trm6 r - rbv6 l) \<union> rfv_trm6 l" |
948 |
948 |
949 instantiation |
949 instantiation |
950 rtrm6 :: pt |
950 rtrm6 :: pt |
951 begin |
951 begin |
952 |
952 |