--- a/Nominal/Nominal2_Eqvt.thy Mon Jan 17 17:20:21 2011 +0100
+++ b/Nominal/Nominal2_Eqvt.thy Tue Jan 18 06:55:18 2011 +0100
@@ -113,11 +113,6 @@
shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
by (perm_simp add: permute_minus_cancel) (rule refl)
-lemma ex1_eqvt[eqvt]:
- shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
- unfolding Ex1_def
- by (perm_simp) (rule refl)
-
lemma ex1_eqvt2:
shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"
by (perm_simp add: permute_minus_cancel) (rule refl)