--- a/Nominal/Nominal2_Base.thy	Fri Mar 19 21:04:24 2010 +0100
+++ b/Nominal/Nominal2_Base.thy	Sat Mar 20 02:46:07 2010 +0100
@@ -412,6 +412,15 @@
   shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))"
 by (simp add: permute_bool_def)
 
+lemma permute_boolE:
+  fixes P::"bool"
+  shows "p \<bullet> P \<Longrightarrow> P"
+  by (simp add: permute_bool_def)
+
+lemma permute_boolI:
+  fixes P::"bool"
+  shows "P \<Longrightarrow> p \<bullet> P"
+  by(simp add: permute_bool_def)
 
 subsection {* Permutations for sets *}