| changeset 1670 | ed89a26b7074 |
| parent 1605 | d46a32cfcd89 |
| child 1673 | e8cf0520c820 |
| 1669:9911824a5396 | 1670:ed89a26b7074 |
|---|---|
3 begin |
3 begin |
4 |
4 |
5 (* Type Schemes *) |
5 (* Type Schemes *) |
6 atom_decl name |
6 atom_decl name |
7 |
7 |
8 (*ML {* val _ = alpha_type := AlphaRes *}*) |
|
8 nominal_datatype t = |
9 nominal_datatype t = |
9 Var "name" |
10 Var "name" |
10 | Fun "t" "t" |
11 | Fun "t" "t" |
11 and tyS = |
12 and tyS = |
12 All xs::"name fset" ty::"t" bind xs in ty |
13 All xs::"name fset" ty::"t" bind xs in ty |