equal
deleted
inserted
replaced
66 |
66 |
67 thm f0_raw.simps |
67 thm f0_raw.simps |
68 |
68 |
69 text {* example type schemes *} |
69 text {* example type schemes *} |
70 |
70 |
|
71 (* does not work yet |
71 nominal_datatype t = |
72 nominal_datatype t = |
72 Var "name" |
73 Var "name" |
73 | Fun "t" "t" |
74 | Fun "t" "t" |
74 |
75 |
75 (* does not work yet |
|
76 nominal_datatype tyS = |
76 nominal_datatype tyS = |
77 All xs::"name list" ty::"t_raw" bind xs in ty |
77 All xs::"name list" ty::"t_raw" bind xs in ty |
78 *) |
78 *) |
79 |
79 |
80 (* also does not work |
|
81 nominal_datatype t = |
80 nominal_datatype t = |
82 Var "name" |
81 Var "name" |
83 | Fun "t" "t" |
82 | Fun "t" "t" |
84 and tyS = |
83 and tyS = |
85 All xs::"name list" ty::"t" bind xs in ty |
84 All xs::"name set" ty::"t" bind xs in ty |
86 *) |
|
87 |
85 |
88 (* example 1 from Terms.thy *) |
86 (* example 1 from Terms.thy *) |
89 |
87 |
90 nominal_datatype trm1 = |
88 nominal_datatype trm1 = |
91 Vr1 "name" |
89 Vr1 "name" |