diff -r 69ef734825c5 -r 8bcc8809ed3b src/HOL/Nominal/Examples/CR.thy
--- a/src/HOL/Nominal/Examples/CR.thy	Thu Apr 19 16:27:53 2007 +0200
+++ b/src/HOL/Nominal/Examples/CR.thy	Thu Apr 19 16:38:59 2007 +0200
@@ -155,6 +155,8 @@
   | b3[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [a].s2)"
   | b4[intro]: "a\<sharp>s2 \<Longrightarrow> (App (Lam [a].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"
 
+equivariance Beta
+
 nominal_inductive Beta
   by (simp_all add: abs_fresh fresh_fact')
 
@@ -183,6 +185,8 @@
   | o3[simp,intro!]: "s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>1(Lam [a].s2)"
   | o4[simp,intro!]: "\<lbrakk>a\<sharp>(s1,s2); s1\<longrightarrow>\<^isub>1s2;t1\<longrightarrow>\<^isub>1t2\<rbrakk> \<Longrightarrow> (App (Lam [a].t1) s1)\<longrightarrow>\<^isub>1(t2[a::=s2])"
 
+equivariance One
+
 nominal_inductive One
   by (simp_all add: abs_fresh fresh_fact')