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