equal
deleted
inserted
replaced
18 bv |
18 bv |
19 where |
19 where |
20 "bv (Bar0 x) = {}" |
20 "bv (Bar0 x) = {}" |
21 | "bv (Bar1 v x b) = {atom v}" |
21 | "bv (Bar1 v x b) = {atom v}" |
22 |
22 |
|
23 thm foo_bar.perm_bn_alpha |
|
24 thm foo_bar.perm_bn_simps |
|
25 thm foo_bar.bn_finite |
|
26 |
|
27 thm foo_bar.eq_iff |
23 thm foo_bar.distinct |
28 thm foo_bar.distinct |
24 thm foo_bar.induct |
29 thm foo_bar.induct |
25 thm foo_bar.inducts |
30 thm foo_bar.inducts |
26 thm foo_bar.exhaust |
31 thm foo_bar.exhaust |
27 thm foo_bar.fv_defs |
32 thm foo_bar.fv_defs |