--- a/Nominal/Ex/SingleLet.thy	Sun Aug 29 12:17:25 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Sun Aug 29 13:36:03 2010 +0800
@@ -1,5 +1,5 @@
 theory SingleLet
-imports "../NewParser"
+imports "../Nominal2"
 begin
 
 atom_decl name
@@ -38,17 +38,19 @@
 
 
 
-
+(*
 lemma test: 
   "(\<exists>p. (bs, x) \<approx>lst (op=) f p (cs, y)) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))"
-sorry
+oops
 
 lemma Abs_eq_iff:
   shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
   and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
   and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
   by (lifting alphas_abs)
+*)
 
+(*
 lemma supp_fv:
   "supp t = fv_trm t \<and> supp b = fv_bn b"
 apply(rule single_let.induct)
@@ -73,7 +75,7 @@
 apply(subst test)
 apply(rule refl)
 sorry
-
+*)
 (*
 consts perm_bn_trm :: "perm \<Rightarrow> trm \<Rightarrow> trm"
 consts perm_bn_assg :: "perm \<Rightarrow> assg \<Rightarrow> assg"