| changeset 2389 | 0f24c961b5f6 |
| parent 2388 | ebf253d80670 |
| child 2392 | 9294d7cec5e2 |
| 2388:ebf253d80670 | 2389:0f24c961b5f6 |
|---|---|
19 binder |
19 binder |
20 bn::"assg \<Rightarrow> atom set" |
20 bn::"assg \<Rightarrow> atom set" |
21 where |
21 where |
22 "bn (As x y t) = {atom x}" |
22 "bn (As x y t) = {atom x}" |
23 |
23 |
24 thm alpha_sym_thms |
|
25 thm alpha_trans_thms |
|
24 thm size_eqvt |
26 thm size_eqvt |
25 thm alpha_bn_imps |
27 thm alpha_bn_imps |
26 thm distinct |
28 thm distinct |
27 thm eq_iff |
29 thm eq_iff |
28 thm eq_iff_simps |
30 thm eq_iff_simps |