changeset 2625 | 478c5648e73f |
parent 2611 | 3d101f2f817c |
child 2950 | 0911cb7bf696 |
--- a/Nominal/Ex/Ex1.thy Wed Dec 22 23:12:51 2010 +0000 +++ b/Nominal/Ex/Ex1.thy Thu Dec 23 00:22:41 2010 +0000 @@ -40,8 +40,8 @@ thm foo_bar.supp lemma - "fv_foo (Foo1 (Bar1 v x (Bar0 x)) (Foo0 v)) = {}" -apply(simp only: foo_bar.fv_defs) + "supp (Foo1 (Bar1 v x (Bar0 x)) (Foo0 v)) = {}" +apply(simp only: foo_bar.supp) apply(simp only: foo_bar.bn_defs) apply(simp only: supp_at_base) apply(simp)