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 (* does not work yet |
72 nominal_datatype t = |
72 nominal_datatype t = |
73 Var "name" |
73 Var "name" |
74 | Fun "t" "t" |
74 | Fun "t" "t" |
75 |
75 |
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" |
135 "bv3 ANil = {}" |
133 "bv3 ANil = {}" |
136 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
134 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
137 |
135 |
138 (* example 4 from Terms.thy *) |
136 (* example 4 from Terms.thy *) |
139 |
137 |
140 (* does not work yet |
138 |
141 nominal_datatype trm4 = |
139 nominal_datatype trm4 = |
142 Vr4 "name" |
140 Vr4 "name" |
143 | Ap4 "trm4" "trm4 list" |
141 | Ap4 "trm4" "trm4 list" |
144 | Lm4 x::"name" t::"trm4" bind x in t |
142 | Lm4 x::"name" t::"trm4" bind x in t |
145 *) |
143 |
146 |
144 |
147 (* example 5 from Terms.thy *) |
145 (* example 5 from Terms.thy *) |
148 |
146 |
149 nominal_datatype trm5 = |
147 nominal_datatype trm5 = |
150 Vr5 "name" |
148 Vr5 "name" |