--- 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"