# HG changeset patch
# User narboux
# Date 1177416136 -7200
# Node ID d08efe73b27f04fb37886a0230f998e3e89f32c5
# Parent  8c64803fae4874d128433a4296d9af05acd93f5b
oups : wrong commit

diff -r 8c64803fae48 -r d08efe73b27f src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Tue Apr 24 14:01:23 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Tue Apr 24 14:02:16 2007 +0200
@@ -634,10 +634,6 @@
   shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1) \<triangleq> (rev pi2)"
   by (simp add: at_prm_rev_eq[OF at])
 
-lemma at_perm_fresh_fresh:
-  fixes a  :: "'x"
-  assumes 
-
 
 lemma at_ds1:
   fixes a  :: "'x"