diff -r d3fe17786640 -r 226b797868dc Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Thu Apr 15 21:56:03 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Fri Apr 16 10:18:16 2010 +0200
@@ -180,21 +180,35 @@
 inductive
  alpha_lam_raw'
 where
-  "name = namea \<Longrightarrow> alpha_lam_raw' (Var_raw name) (Var_raw namea)"
-| "\<lbrakk>alpha_lam_raw' lam_raw1 lam_raw1a; alpha_lam_raw' lam_raw2 lam_raw2a\<rbrakk> \<Longrightarrow>
+  a1: "name = namea \<Longrightarrow> alpha_lam_raw' (Var_raw name) (Var_raw namea)"
+| a2: "\<lbrakk>alpha_lam_raw' lam_raw1 lam_raw1a; alpha_lam_raw' lam_raw2 lam_raw2a\<rbrakk> \<Longrightarrow>
    alpha_lam_raw' (App_raw lam_raw1 lam_raw2) (App_raw lam_raw1a lam_raw2a)"
-| "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow>
+| a3: "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow>
    alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)"
 
 declare permute_lam_raw.simps[eqvt]
-(*declare alpha_gen_real_eqvt[eqvt]*)
+declare alpha_gen_eqvt[eqvt]
 (*equivariance alpha_lam_raw'*)
+thm eqvts_raw
+
+lemma
+  assumes a: "alpha_lam_raw' t1 t2"
+  shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)"
+oops
 
 lemma
   assumes a: "alpha_lam_raw' t1 t2"
   shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)"
 using a
 apply(induct)
+ML_prf {*
+val ({names, ...}, {raw_induct, intrs, ...}) =
+    Inductive.the_inductive @{context} (Sign.intern_const @{theory} "alpha_lam_raw")
+*}
+apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac 
+  @{context} ["Lambda.alpha_lam_raw"] @{term "p::perm"} @{thm a1} 1*})
+apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac 
+  @{context} ["Lambda.alpha_lam_raw"] @{term "p::perm"} @{thm a2} 1*})
 oops