equal
deleted
inserted
replaced
3 begin |
3 begin |
4 |
4 |
5 section {*** Type Schemes ***} |
5 section {*** Type Schemes ***} |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 declare [[STEPS = 9]] |
8 |
|
9 declare [[STEPS = 15]] |
9 |
10 |
10 nominal_datatype ty = |
11 nominal_datatype ty = |
11 Var "name" |
12 Var "name" |
12 | Fun "ty" "ty" |
13 | Fun "ty" "ty" |
13 and tys = |
14 and tys = |
15 |
16 |
16 nominal_datatype ty2 = |
17 nominal_datatype ty2 = |
17 Var2 "name" |
18 Var2 "name" |
18 | Fun2 "ty2" "ty2" |
19 | Fun2 "ty2" "ty2" |
19 |
20 |
20 (* PROBLEM: this only works once the type is defined |
21 instance ty2 :: pt sorry |
|
22 |
21 nominal_datatype tys2 = |
23 nominal_datatype tys2 = |
22 All2 xs::"name fset" ty::"ty2" bind_res xs in ty |
24 All2 xs::"name fset" ty::"ty2" bind_res xs in ty |
23 *) |
25 |
24 |
26 |
25 lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp] |
27 lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp] |
26 |
28 |
27 |
29 |
28 |
30 |