equal
deleted
inserted
replaced
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 ML {* val _ = recursive := false *} |
7 ML {* val _ = recursive := false *} |
8 |
|
9 nominal_datatype trm0 = |
|
10 Var0 "name" |
|
11 | App0 "trm0" "trm0" |
|
12 | Lam0 x::"name" t::"trm0" bind x in t |
|
13 | Let0 p::"pat0" "trm0" t::"trm0" bind "f0 p" in t |
|
14 and pat0 = |
|
15 PN0 |
|
16 | PS0 "name" |
|
17 | PD0 "pat0" "pat0" |
|
18 binder |
|
19 f0::"pat0 \<Rightarrow> atom set" |
|
20 where |
|
21 "f0 PN0 = {}" |
|
22 | "f0 (PS0 x) = {atom x}" |
|
23 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)" |
|
24 |
|
25 thm trm0_pat0.fv |
|
26 thm trm0_pat0.eq_iff |
|
27 thm trm0_pat0.bn |
|
28 thm trm0_pat0.perm |
|
29 thm trm0_pat0.induct |
|
30 thm trm0_pat0.distinct |
|
31 thm trm0_pat0.fv[simplified trm0_pat0.supp,no_vars] |
|
32 |
8 |
33 (* example 1 from Terms.thy *) |
9 (* example 1 from Terms.thy *) |
34 |
10 |
35 nominal_datatype trm1 = |
11 nominal_datatype trm1 = |
36 Vr1 "name" |
12 Vr1 "name" |