--- a/Nominal/Ex/Lambda_add.thy	Fri Jun 24 11:14:58 2011 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-theory Lambda_add
-imports "Lambda"
-begin
-
-nominal_primrec
-  addlam :: "lam \<Rightarrow> lam"
-where
-  "fv \<noteq> x \<Longrightarrow> addlam (Var x) = Lam [fv]. App (Var fv) (Var x)"
-| "addlam (App t1 t2) = App t1 t2"
-| "addlam (Lam [x]. t) = Lam [x].t"
-  unfolding addlam_graph_def eqvt_def
-  apply perm_simp
-  apply auto
-  apply (case_tac x rule: lam.exhaust)
-  apply auto
-  apply (rule_tac x="name" and ?'a="name" in obtain_fresh)
-  apply (simp add: fresh_at_base)
-  apply (simp add: Abs1_eq_iff lam.fresh fresh_at_base)
-  done
-
-termination by lexicographic_order
-
-end