equal
deleted
inserted
replaced
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 nominal_datatype trm = |
7 nominal_datatype trm = |
8 Vr "name" |
8 Var "name" |
9 | Ap "trm" "trm" |
9 | App "trm" "trm" |
10 | Lm x::"name" t::"trm" binds (set) x in t |
10 | Lam x::"name" t::"trm" binds x in t |
11 | Lt a::"lts" t::"trm" binds "bn a" in a t |
11 | Let as::"assn" t::"trm" binds "bn as" in t |
12 and lts = |
12 | Let_rec as::"assn" t::"trm" binds "bn as" in as t |
13 Lnil |
13 and assn = |
14 | Lcons "name" "trm" "lts" |
14 ANil |
|
15 | ACons "name" "trm" "assn" |
15 binder |
16 binder |
16 bn |
17 bn |
17 where |
18 where |
18 "bn Lnil = []" |
19 "bn (ANil) = []" |
19 | "bn (Lcons x t l) = (atom x) # (bn l)" |
20 | "bn (ACons x t as) = (atom x) # (bn as)" |
20 |
21 |
|
22 thm trm_assn.eq_iff |
|
23 thm trm_assn.supp |
21 |
24 |
22 thm trm_lts.fv_defs |
25 thm trm_assn.fv_defs |
23 thm trm_lts.eq_iff |
26 thm trm_assn.eq_iff |
24 thm trm_lts.bn_defs |
27 thm trm_assn.bn_defs |
25 thm trm_lts.perm_simps |
28 thm trm_assn.perm_simps |
26 thm trm_lts.induct |
29 thm trm_assn.induct |
27 thm trm_lts.distinct |
30 thm trm_assn.distinct |
28 |
31 |
29 |
32 |
30 |
33 |
31 section {* Tests *} |
34 section {* Tests *} |
32 |
35 |