equal
deleted
inserted
replaced
38 thm foo_bar.supports |
38 thm foo_bar.supports |
39 thm foo_bar.fsupp |
39 thm foo_bar.fsupp |
40 thm foo_bar.supp |
40 thm foo_bar.supp |
41 |
41 |
42 lemma |
42 lemma |
43 "fv_foo (Foo1 (Bar1 v x (Bar0 x)) (Foo0 v)) = {}" |
43 "supp (Foo1 (Bar1 v x (Bar0 x)) (Foo0 v)) = {}" |
44 apply(simp only: foo_bar.fv_defs) |
44 apply(simp only: foo_bar.supp) |
45 apply(simp only: foo_bar.bn_defs) |
45 apply(simp only: foo_bar.bn_defs) |
46 apply(simp only: supp_at_base) |
46 apply(simp only: supp_at_base) |
47 apply(simp) |
47 apply(simp) |
48 done |
48 done |
49 |
49 |