| changeset 1117 | 8948319b190e |
| parent 1111 | ee276c9f12f0 |
| child 1119 | 44cabac6ad3d |
| 1116:3acc7d25627a | 1117:8948319b190e |
|---|---|
934 |
934 |
935 primrec |
935 primrec |
936 rbv6 |
936 rbv6 |
937 where |
937 where |
938 "rbv6 (rVr6 n) = {}" |
938 "rbv6 (rVr6 n) = {}" |
939 | "rbv6 (rLm6 n t) = {atom n}" |
939 | "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t" |
940 | "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r" |
940 | "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r" |
941 |
941 |
942 primrec |
942 primrec |
943 rfv_trm6 |
943 rfv_trm6 |
944 where |
944 where |