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