diff -r 69ef734825c5 -r 8bcc8809ed3b 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 \ \ \ \ Const n : TBase" | t_Unit[intro]: "valid \ \ \ \ Unit : TUnit" +equivariance typing + nominal_inductive typing by (simp_all add: abs_fresh) @@ -340,6 +342,8 @@ | Q_Ext[intro]: "\x\(\,s,t); (x,T\<^isub>1)#\ \ App s (Var x) \ App t (Var x) : T\<^isub>2\ \ \ \ s \ t : T\<^isub>1 \ 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]: "\\ \ p \ q : T\<^isub>1 \ T\<^isub>2; \ \ s \ t : T\<^isub>1\ \ \ \ App p s \ App q t : T\<^isub>2" | QAP_Const[intro]: "valid \ \ \ \ Const n \ Const n : TBase" +equivariance alg_equiv + nominal_inductive alg_equiv avoids QAT_Arrow: x by simp_all