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 (* example 1 from Terms.thy *) |
|
10 |
|
11 nominal_datatype trm1 = |
|
12 Vr1 "name" |
|
13 | Ap1 "trm1" "trm1" |
|
14 | Lm1 x::"name" t::"trm1" bind x in t |
|
15 | Lt1 p::"bp1" "trm1" t::"trm1" bind "bv1 p" in t |
|
16 and bp1 = |
|
17 BUnit1 |
|
18 | BV1 "name" |
|
19 | BP1 "bp1" "bp1" |
|
20 binder |
|
21 bv1 |
|
22 where |
|
23 "bv1 (BUnit1) = {}" |
|
24 | "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
|
25 | "bv1 (BV1 x) = {atom x}" |
|
26 |
|
27 thm trm1_bp1.fv |
|
28 thm trm1_bp1.eq_iff |
|
29 thm trm1_bp1.bn |
|
30 thm trm1_bp1.perm |
|
31 thm trm1_bp1.induct |
|
32 thm trm1_bp1.distinct |
|
33 thm trm1_bp1.fv[simplified trm1_bp1.supp] |
|
34 |
8 |
35 text {* example 3 from Terms.thy *} |
9 text {* example 3 from Terms.thy *} |
36 |
10 |
37 nominal_datatype trm3 = |
11 nominal_datatype trm3 = |
38 Vr3 "name" |
12 Vr3 "name" |