# HG changeset patch
# User urbanc
# Date 1174643403 -3600
# Node ID ca326e0fb5c50a7685755ac798f512c064875306
# Parent  d284097414065c7fa90603f43010679551a88fb9
added the permutation operation on options to the list of equivariance lemmas

diff -r d28409741406 -r ca326e0fb5c5 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Fri Mar 23 09:46:22 2007 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Fri Mar 23 10:50:03 2007 +0100
@@ -3152,6 +3152,7 @@
   perm_list.simps append_eqvt
   perm_prod.simps
   fst_eqvt snd_eqvt
+  perm_option.simps
 
   (* nats *)
   Suc_eqvt Zero_nat_eqvt One_nat_eqvt min_nat_eqvt max_nat_eqvt