# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1283361386 -28800
# Node ID 16d32eddc17fd949dba46325844235c4e0bc9564
# Parent  ac3470e1e5af4109abfb7e62804bd6309d215b52
added eqvt-attribute for permute_abs lemmas

diff -r ac3470e1e5af -r 16d32eddc17f Nominal/Abs.thy
--- a/Nominal/Abs.thy	Tue Aug 31 21:03:08 2010 +0800
+++ b/Nominal/Abs.thy	Thu Sep 02 01:16:26 2010 +0800
@@ -368,7 +368,7 @@
 
 end
 
-lemmas permute_abs = permute_Abs permute_Abs_res permute_Abs_lst
+lemmas permute_abs[eqvt] = permute_Abs permute_Abs_res permute_Abs_lst
 
 
 lemma abs_swap1: