--- a/Nominal/Ex/Lambda.thy	Tue Jul 19 01:40:36 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Tue Jul 19 02:30:05 2011 +0100
@@ -45,18 +45,10 @@
 
 termination (eqvt) by lexicographic_order
 
-ML {*
-Item_Net.content (Nominal_Function_Common.get_function @{context})
-*}
-
 thm is_app_def
+thm is_app.eqvt
 
-
-lemma [eqvt]:
-  shows "(p \<bullet> (is_app t)) = is_app (p \<bullet> t)"
-apply(induct t rule: lam.induct)
-apply(simp_all add: permute_bool_def)
-done
+thm eqvts
 
 nominal_primrec 
   rator :: "lam \<Rightarrow> lam option"
@@ -74,12 +66,6 @@
 
 termination (eqvt) by lexicographic_order
 
-lemma [eqvt]:
-  shows "(p \<bullet> (rator t)) = rator (p \<bullet> t)"
-apply(induct t rule: lam.induct)
-apply(simp_all)
-done
-
 nominal_primrec 
   rand :: "lam \<Rightarrow> lam option"
 where
@@ -96,12 +82,6 @@
 
 termination (eqvt) by lexicographic_order
 
-lemma [eqvt]:
-  shows "(p \<bullet> (rand t)) = rand (p \<bullet> t)"
-apply(induct t rule: lam.induct)
-apply(simp_all)
-done
-
 nominal_primrec 
   is_eta_nf :: "lam \<Rightarrow> bool"
 where
@@ -162,11 +142,6 @@
 apply(rule refl)
 done
 
-thm inl_eqvt
-thm var_pos_def
-
-thm fun_eq_iff
-
 termination (eqvt) by lexicographic_order
 
 lemma var_pos1:
@@ -315,9 +290,7 @@
 termination (eqvt)
   by lexicographic_order
 
-lemma subst_eqvt[eqvt]:
-  shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]"
-by (induct t x s rule: subst.induct) (simp_all)
+thm subst.eqvt
 
 lemma forget:
   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"