equal
deleted
inserted
replaced
17 binder |
17 binder |
18 bn::"assg \<Rightarrow> atom set" |
18 bn::"assg \<Rightarrow> atom set" |
19 where |
19 where |
20 "bn (As x t) = {atom x}" |
20 "bn (As x t) = {atom x}" |
21 |
21 |
22 thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] |
22 thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] bn_raw.simps[no_vars] |
23 |
23 |
24 ML {* Inductive.the_inductive *} |
24 ML {* Inductive.the_inductive *} |
25 thm trm_assg.fv |
25 thm trm_assg.fv |
26 thm trm_assg.supp |
26 thm trm_assg.supp |
27 thm trm_assg.eq_iff |
27 thm trm_assg.eq_iff |