--- a/Nominal/Ex/Lambda.thy	Sun Apr 11 22:48:49 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Mon Apr 12 13:34:54 2010 +0200
@@ -132,8 +132,14 @@
         atac ])
 *}
 
+ML {* try hd [1] *}
 
-lemma 
+ML {*
+Skip_Proof.cheat_tac
+*}
+
+
+lemma [eqvt]:
   assumes a: "valid Gamma" 
   shows "valid (p \<bullet> Gamma)"
 using a
@@ -142,13 +148,8 @@
 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *})
 done
 
-lemma
-  "(p \<bullet> valid) = valid"
-oops
-
-lemma temp[eqvt_raw]: 
-  "(p \<bullet> valid) \<equiv> valid"
-sorry
+thm eqvts
+thm eqvts_raw
 
 inductive
   typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
@@ -157,7 +158,7 @@
   | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
   | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2"
 
-lemma
+lemma uu[eqvt]:
   assumes a: "Gamma \<turnstile> t : T" 
   shows "(p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)"
 using a
@@ -167,6 +168,9 @@
 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
 done
 
+thm eqvts
+thm eqvts_raw
+
 declare permute_lam_raw.simps[eqvt]
 
 thm alpha_gen_real_eqvt[no_vars]