diff -r 66ae73fd66c0 -r 29ebbe56f450 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Tue Aug 17 06:39:27 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Tue Aug 17 06:50:49 2010 +0800
@@ -29,10 +29,9 @@
 thm perm_simps
 thm perm_laws
 thm trm_raw_assg_raw.size(9 - 16)
-
-(* cannot lift yet *)
 thm eq_iff
 thm eq_iff_simps
+
 (* bn / eqvt lemmas for fv / fv_bn / bn *)
 
 ML {*
@@ -59,18 +58,21 @@
   val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws}
 *}
 
-
-section {* NOT *} 
-
 ML {*
  val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) 
    @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
     prod.cases]}
 *}
 
-
+ML {*
+ val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) 
+   @{thms eq_iff_simps[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
+    prod.cases]}
+*}
 
-
+ML {*
+  val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms bn_defs}
+*}
 
 thm perm_defs
 thm perm_simps