# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271606165 -7200
# Node ID b5776e0a015f066ecaaf140adb46ba8e6f756c15
# Parent  26c0c35641cbf944582273708c2a053a6a129fc0
tuned

diff -r 26c0c35641cb -r b5776e0a015f Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Sun Apr 18 10:58:29 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Sun Apr 18 17:56:05 2010 +0200
@@ -2,8 +2,8 @@
     Author:     Brian Huffman, 
     Author:     Christian Urban
 
-    Equivariance, Supp and Fresh Lemmas for Operators. 
-    (Contains many, but not all such lemmas.)
+    Equivariance, supp and freshness lemmas for various operators 
+    (contains many, but not all such lemmas).
 *)
 theory Nominal2_Eqvt
 imports Nominal2_Base Nominal2_Atoms
@@ -12,7 +12,6 @@
      ("nominal_eqvt.ML")
 begin
 
-
 section {* Logical Operators *}
 
 lemma eq_eqvt:
@@ -238,7 +237,9 @@
 
 section {* Equivariance automation *}
 
-text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_force} *}
+text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}
+
+ML {* Thm.declaration_attribute *}
 
 use "nominal_thmdecls.ML"
 setup "Nominal_ThmDecls.setup"