# HG changeset patch
# User narboux
# Date 1171559901 -3600
# Node ID a3acee47a8831a8ccb3383c2349978550e44d94e
# Parent  be61bd159a999c00eda6fdd99dfa92753b8adf04
start adding the attribute eqvt to some lemmas of the nominal library

diff -r be61bd159a99 -r a3acee47a883 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Thu Feb 15 17:35:19 2007 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Thu Feb 15 18:18:21 2007 +0100
@@ -3008,6 +3008,10 @@
 use "nominal_thmdecls.ML"
 setup "NominalThmDecls.setup"
 
+lemmas  [eqvt] = perm_list.simps perm_prod.simps 
+
+
+
 (***************************************)
 (* setup for the individial atom-kinds *)
 (* and nominal datatypes               *)