author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
Mon, 22 Mar 2010 09:02:30 +0100 | |
changeset 1567 | 8f28e749d92b |
parent 1566 | 2facd6645599 |
child 1568 | 2311a9fc4624 |
--- 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