--- 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')