equal
deleted
inserted
replaced
1 theory SingleLetFoo |
1 theory SingleLetFoo |
2 imports "../NewParser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 |
5 |
6 declare [[STEPS = 4]] |
6 declare [[STEPS = 5]] |
7 (* alpha does not work for this type *) |
|
8 |
7 |
9 atom_decl name |
8 atom_decl name |
10 |
9 |
11 nominal_datatype trm = |
10 nominal_datatype trm = |
12 Var "name" |
11 Var "name" |
19 As "name" "trm" |
18 As "name" "trm" |
20 binder |
19 binder |
21 bn::"assg \<Rightarrow> atom set" |
20 bn::"assg \<Rightarrow> atom set" |
22 where |
21 where |
23 "bn (As x t) = {atom x}" |
22 "bn (As x t) = {atom x}" |
|
23 |
|
24 thm trm_assg.distinct |
|
25 thm trm_assg.eq_iff |
|
26 thm trm_assg.supp |
|
27 thm trm_assg.perm |
24 |
28 |
25 thm permute_trm_raw_permute_assg_raw.simps |
29 thm permute_trm_raw_permute_assg_raw.simps |
26 thm fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps[no_vars] |
30 thm fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps[no_vars] |
27 |
31 |
28 (* there is something wrong with the free variables *) |
32 (* there is something wrong with the free variables *) |