| changeset 2450 | 217ef3e4282e |
| parent 2436 | 3885dc2669f9 |
| child 2451 | d2e929f51fa9 |
| 2449:6b51117b8955 | 2450:217ef3e4282e |
|---|---|
16 |
16 |
17 |
17 |
18 nominal_datatype ty2 = |
18 nominal_datatype ty2 = |
19 Var2 "name" |
19 Var2 "name" |
20 | Fun2 "ty2" "ty2" |
20 | Fun2 "ty2" "ty2" |
21 |
|
22 instantiation ty2 :: fs |
|
23 begin |
|
24 |
|
25 instance |
|
26 sorry |
|
27 |
|
28 end |
|
29 |
|
21 |
30 |
22 nominal_datatype tys2 = |
31 nominal_datatype tys2 = |
23 All2 xs::"name fset" ty::"ty2" bind (res) xs in ty |
32 All2 xs::"name fset" ty::"ty2" bind (res) xs in ty |
24 |
33 |
25 |
34 |