equal
deleted
inserted
replaced
14 binder |
14 binder |
15 bn::"assg \<Rightarrow> atom set" |
15 bn::"assg \<Rightarrow> atom set" |
16 where |
16 where |
17 "bn (As x t) = {atom x}" |
17 "bn (As x t) = {atom x}" |
18 |
18 |
19 |
19 ML {* Inductive.the_inductive *} |
20 thm trm_assg.fv |
20 thm trm_assg.fv |
21 thm trm_assg.supp |
21 thm trm_assg.supp |
22 thm trm_assg.eq_iff |
22 thm trm_assg.eq_iff |
23 thm trm_assg.bn |
23 thm trm_assg.bn |
24 thm trm_assg.perm |
24 thm trm_assg.perm |
29 thm trm_assg.fv[simplified trm_assg.supp(1-2)] |
29 thm trm_assg.fv[simplified trm_assg.supp(1-2)] |
30 |
30 |
31 equivariance alpha_trm_raw |
31 equivariance alpha_trm_raw |
32 |
32 |
33 |
33 |
|
34 |
34 end |
35 end |
35 |
36 |
36 |
37 |
37 |
38 |