changeset 1571 | 1d70813ae674 |
parent 1567 | 8f28e749d92b |
child 1633 | 9e31248a1b8c |
--- a/Nominal/Nominal2_Supp.thy Mon Mar 22 10:20:57 2010 +0100 +++ b/Nominal/Nominal2_Supp.thy Mon Mar 22 10:21:14 2010 +0100 @@ -468,7 +468,7 @@ section {* at_set_avoiding2 *} -lemma at_set_avoiding2 +lemma at_set_avoiding2: assumes "finite xs" and "finite (supp c)" "finite (supp x)" and "xs \<sharp>* x" @@ -483,4 +483,4 @@ apply(auto simp add: fresh_star_def fresh_def) done -end \ No newline at end of file +end