diff -r 69ef734825c5 -r 8bcc8809ed3b src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Thu Apr 19 16:27:53 2007 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Thu Apr 19 16:38:59 2007 +0200
@@ -269,6 +269,8 @@
                    (x\<^isub>1,Data(S\<^isub>1))#\<Gamma> \<turnstile> e\<^isub>1 : T; (x\<^isub>2,Data(S\<^isub>2))#\<Gamma> \<turnstile> e\<^isub>2 : T\<rbrakk> 
                    \<Longrightarrow> \<Gamma> \<turnstile> (Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2) : T"
 
+equivariance typing
+
 nominal_inductive typing
   by (simp_all add: abs_fresh fresh_prod fresh_atm)
 
@@ -499,6 +501,8 @@
 | b_CaseR[intro]: "\<lbrakk>x\<^isub>1\<sharp>(e,e\<^isub>2,e'',x\<^isub>2); x\<^isub>2\<sharp>(e,e\<^isub>1,e'',x\<^isub>1) ; e\<Down>InR e'; e\<^isub>2[x\<^isub>2::=e']\<Down>e''\<rbrakk> 
                    \<Longrightarrow> Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 \<Down> e''"
 
+equivariance big
+
 nominal_inductive big
   by (simp_all add: abs_fresh fresh_prod fresh_atm)