| changeset 1284 | 212f3ab40cc2 |
| parent 1283 | 6a133abb7633 |
| child 1285 | e3ac56d3b7af |
| 1283:6a133abb7633 | 1284:212f3ab40cc2 |
|---|---|
196 where |
196 where |
197 "bv9 (Var9 x) = {}" |
197 "bv9 (Var9 x) = {}" |
198 | "bv9 (Lam9 x b) = {atom x}" |
198 | "bv9 (Lam9 x b) = {atom x}" |
199 |
199 |
200 (* example form Leroy 96 about modules *) |
200 (* example form Leroy 96 about modules *) |
201 |
|
201 |
202 |
202 nominal_datatype mexp = |
203 nominal_datatype mexp = |
203 Acc path |
204 Acc path |
204 | Stru body |
205 | Stru body |
205 | Funct x::name sexp m::mexp bind x in m |
206 | Funct x::name sexp m::mexp bind x in m |