| changeset 2480 | ac7dff1194e8 |
| parent 2454 | 9ffee4eb1ae1 |
| child 2481 | 3a5ebb2fcdbf |
| 2479:a9b6a00b1ba0 | 2480:ac7dff1194e8 |
|---|---|
4 |
4 |
5 (* example from Leroy'96 about modules; |
5 (* example from Leroy'96 about modules; |
6 see OTT example by Owens *) |
6 see OTT example by Owens *) |
7 |
7 |
8 atom_decl name |
8 atom_decl name |
9 |
|
10 declare [[STEPS = 31]] |
|
11 |
|
9 |
12 |
10 nominal_datatype modules: |
13 nominal_datatype modules: |
11 mexp = |
14 mexp = |
12 Acc "path" |
15 Acc "path" |
13 | Stru "body" |
16 | Stru "body" |