equal
deleted
inserted
replaced
16 bv |
16 bv |
17 where |
17 where |
18 "bv (Bar0 x) = {}" |
18 "bv (Bar0 x) = {}" |
19 | "bv (Bar1 v x b) = {atom v}" |
19 | "bv (Bar1 v x b) = {atom v}" |
20 |
20 |
21 |
21 thm foo_bar.distinct |
22 thm foo_bar.fv_defs[no_vars] foo_bar.bn_defs[no_vars] |
22 thm foo_bar.induct |
|
23 thm foo_bar.inducts |
|
24 thm foo_bar.exhaust |
|
25 thm foo_bar.fv_defs |
|
26 thm foo_bar.bn_defs |
|
27 thm foo_bar.perm_simps |
|
28 thm foo_bar.eq_iff |
|
29 thm foo_bar.fv_bn_eqvt |
|
30 thm foo_bar.size_eqvt |
|
31 thm foo_bar.supports |
|
32 thm foo_bar.fsupp |
|
33 thm foo_bar.supp |
23 |
34 |
24 lemma |
35 lemma |
25 "fv_foo (Foo1 (Bar1 v x (Bar0 x)) (Foo0 v)) = {}" |
36 "fv_foo (Foo1 (Bar1 v x (Bar0 x)) (Foo0 v)) = {}" |
26 apply(simp only: foo_bar.fv_defs) |
37 apply(simp only: foo_bar.fv_defs) |
27 apply(simp only: foo_bar.bn_defs) |
38 apply(simp only: foo_bar.bn_defs) |