--- a/src/HOL/Nominal/Examples/SN.thy Thu Apr 19 16:27:53 2007 +0200
+++ b/src/HOL/Nominal/Examples/SN.thy Thu Apr 19 16:38:59 2007 +0200
@@ -66,6 +66,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')
@@ -166,6 +168,8 @@
| t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
| t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
+equivariance typing
+
nominal_inductive typing
by (simp_all add: abs_fresh fresh_ty)