equal
deleted
inserted
replaced
38 binder |
38 binder |
39 f::"pat' \<Rightarrow> name set" |
39 f::"pat' \<Rightarrow> name set" |
40 where |
40 where |
41 "f PN = {}" |
41 "f PN = {}" |
42 | "f (PS x) = {x}" |
42 | "f (PS x) = {x}" |
43 | "f (PD x y) = {x,y}" |
43 | "f (PD x y) = {x, y}" |
44 |
44 |
45 thm f_raw.simps |
45 thm f_raw.simps |
46 |
46 |
47 nominal_datatype trm0 = |
47 nominal_datatype trm0 = |
48 Var0 "name" |
48 Var0 "name" |
76 (* example 1 from Terms.thy *) |
76 (* example 1 from Terms.thy *) |
77 |
77 |
78 nominal_datatype trm1 = |
78 nominal_datatype trm1 = |
79 Vr1 "name" |
79 Vr1 "name" |
80 | Ap1 "trm1" "trm1" |
80 | Ap1 "trm1" "trm1" |
81 | Lm1 x::"name" t::"trm1" bind x in t |
81 | Lm1 x::"name" t::"trm1" bind x in t |
82 | Lt1 p::"bp1" "trm1" t::"trm1" bind "bv1 p" in t |
82 | Lt1 p::"bp1" "trm1" t::"trm1" bind "bv1 p" in t |
83 and bp1 = |
83 and bp1 = |
84 BUnit1 |
84 BUnit1 |
85 | BV1 "name" |
85 | BV1 "name" |
86 | BP1 "bp1" "bp1" |
86 | BP1 "bp1" "bp1" |
201 (* example from my PHD *) |
201 (* example from my PHD *) |
202 |
202 |
203 atom_decl coname |
203 atom_decl coname |
204 |
204 |
205 nominal_datatype phd = |
205 nominal_datatype phd = |
206 Ax name coname |
206 Ax "name" "coname" |
207 | Cut n::name t1::phd c::coname t2::phd bind n in t1, bind c in t2 |
207 | Cut n::"coname" 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 |
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 |
209 | AndL1 n::"name" t::"phd" "name" bind n in t |
210 | AndL2 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 |
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 |
212 | ImpR c::"coname" n::"name" t::"phd" "coname" bind n in 1, bind c in t |
213 |
213 |
214 (* example form Leroy 96 about modules; OTT *) |
214 (* example form Leroy 96 about modules; OTT *) |
215 |
215 |
216 nominal_datatype mexp = |
216 nominal_datatype mexp = |
217 Acc path |
217 Acc path |