changeset 1567 | 8f28e749d92b |
parent 1564 | a4743b7cd887 |
child 1633 | 9e31248a1b8c |
--- a/Nominal/Nominal2_Supp.thy Sun Mar 21 22:27:08 2010 +0100 +++ b/Nominal/Nominal2_Supp.thy Mon Mar 22 09:02:30 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