--- a/Nominal/Ex/CR.thy	Wed Dec 21 17:05:00 2011 +0900
+++ b/Nominal/Ex/CR.thy	Thu Dec 22 04:35:01 2011 +0000
@@ -1,5 +1,7 @@
 (* CR_Takahashi from Nominal1 ported to Nominal2 *)
-theory CR imports Nominal2 begin
+theory CR 
+imports "../Nominal2" 
+begin
 
 atom_decl name
 
@@ -86,6 +88,8 @@
   bs1[intro, simp]: "M \<longrightarrow>b* M"
 | bs2[intro]: "\<lbrakk>M1\<longrightarrow>b* M2; M2 \<longrightarrow>b M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>b* M3"
 
+equivariance beta_star
+
 lemma bs3[intro, trans]:
   assumes "A \<longrightarrow>b* B"
   and     "B \<longrightarrow>b* C"