Nominal/Nominal2_Supp.thy
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