# HG changeset patch
# User urbanc
# Date 1189769527 -7200
# Node ID 7be5353ec4bd7550a62eb32b3dd7d4b3cbcdcf84
# Parent  a6d0428dea8e742362c6600b480148f893482a2e
reverted back to the old version of the equivariance lemma for ALL

diff -r a6d0428dea8e -r 7be5353ec4bd src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Thu Sep 13 23:58:38 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Fri Sep 14 13:32:07 2007 +0200
@@ -1766,7 +1766,6 @@
 
 section {* equivaraince for some connectives *}
 
-(*
 lemma pt_all_eqvt:
   fixes  pi :: "'x prm"
   and     x :: "'a"
@@ -1777,18 +1776,6 @@
 apply(drule_tac x="pi\<bullet>x" in spec)
 apply(simp add: pt_rev_pi[OF pt, OF at])
 done
-*)
-
-lemma pt_all_eqvt:
-  fixes  pi :: "'x prm"
-  and     x :: "'a"
-  assumes pt: "pt TYPE('a) TYPE('x)"
-  and     at: "at TYPE('x)"
-  shows "pi\<bullet>(\<forall>(x::'a). P x) = (\<forall>(x::'a). P ((rev pi)\<bullet>x))"
-apply(auto simp add: perm_bool)
-apply(drule_tac x="pi\<bullet>x" in spec)
-apply(simp add: pt_rev_pi[OF pt, OF at])
-done
 
 lemma pt_ex_eqvt:
   fixes  pi :: "'x prm"