src/HOL/Nominal/Examples/Crary.thy

--- a/src/HOL/Nominal/Examples/Crary.thy	Thu Apr 19 16:27:53 2007 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Thu Apr 19 16:38:59 2007 +0200
@@ -304,6 +304,8 @@
 | t_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : TBase"
 | t_Unit[intro]:  "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Unit : TUnit"
 
+equivariance typing
+
 nominal_inductive typing
   by (simp_all add: abs_fresh)
 
@@ -340,6 +342,8 @@
 | Q_Ext[intro]:   "\<lbrakk>x\<sharp>(\<Gamma>,s,t); (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^isub>2\<rbrakk> 
                    \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T\<^isub>1 \<rightarrow> T\<^isub>2"
 
+equivariance def_equiv
+
 nominal_inductive def_equiv
   by (simp_all add: abs_fresh fresh_subst'')
 
@@ -452,6 +456,8 @@
 | QAP_App[intro]:   "\<lbrakk>\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^isub>1 \<rightarrow> T\<^isub>2; \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App p s \<leftrightarrow> App q t : T\<^isub>2"
 | QAP_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n \<leftrightarrow> Const n : TBase"
 
+equivariance alg_equiv
+
 nominal_inductive alg_equiv
   avoids QAT_Arrow: x
   by simp_all