equal
deleted
inserted
replaced
61 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)" |
61 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)" |
62 |
62 |
63 thm f0_raw.simps |
63 thm f0_raw.simps |
64 |
64 |
65 text {* example type schemes *} |
65 text {* example type schemes *} |
|
66 |
66 datatype t = |
67 datatype t = |
67 Var "name" |
68 Var "name" |
68 | Fun "t" "t" |
69 | Fun "t" "t" |
69 |
70 |
70 nominal_datatype tyS = |
71 nominal_datatype tyS = |
195 bv9 |
196 bv9 |
196 where |
197 where |
197 "bv9 (Var9 x) = {}" |
198 "bv9 (Var9 x) = {}" |
198 | "bv9 (Lam9 x b) = {atom x}" |
199 | "bv9 (Lam9 x b) = {atom x}" |
199 |
200 |
200 (* example form Leroy 96 about modules *) |
201 (* example from my PHD *) |
201 |
202 |
|
203 atom_decl coname |
|
204 |
|
205 nominal_datatype phd = |
|
206 Ax name coname |
|
207 | Cut n::name t1::phd c::coname t2::phd bind n in t1, bind c in t2 |
|
208 | AndR c1::coname t1::phd c2::coname t2::phd coname bind c1 in t1, bind c2 in t2 |
|
209 | AndL1 n::name t::phd name bind n in t |
|
210 | AndL2 n::name t::phd name bind n in t |
|
211 | ImpL c::coname t1::phd n::name t2::phd name bind c in t1, bind n in t2 |
|
212 | ImpR c::coname n::name t::phd coname bind n in 1, bind c in t |
|
213 |
|
214 (* example form Leroy 96 about modules; OTT *) |
202 |
215 |
203 nominal_datatype mexp = |
216 nominal_datatype mexp = |
204 Acc path |
217 Acc path |
205 | Stru body |
218 | Stru body |
206 | Funct x::name sexp m::mexp bind x in m |
219 | Funct x::name sexp m::mexp bind x in m |