--- a/Nominal/Ex/SingleLet.thy	Sat Aug 14 16:54:41 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Sat Aug 14 23:33:23 2010 +0800
@@ -4,7 +4,7 @@
 
 atom_decl name
 
-declare [[STEPS = 17]]
+declare [[STEPS = 18]]
 
 nominal_datatype trm  =
   Var "name"
@@ -25,37 +25,13 @@
 thm distinct
 thm trm_raw_assg_raw.inducts
 thm fv_defs
-
-
-(* cannot lift yet *)
-thm eq_iff
-thm eq_iff_simps
 thm perm_simps
 thm perm_laws
 thm trm_raw_assg_raw.size(9 - 16)
 
-(* rsp lemmas *)
-thm size_rsp
-thm funs_rsp
-thm constrs_rsp
-thm permute_rsp
-
-declare constrs_rsp[quot_respect]
-declare funs_rsp[quot_respect] 
-declare size_rsp[quot_respect]
-declare permute_rsp[quot_respect]
-
-ML {*
-  val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct}
-*}
-
-ML {* 
-  val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.inducts}
-*}
-
-ML {*
-  val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs}
-*}
+(* cannot lift yet *)
+thm eq_iff
+thm eq_iff_simps
 
 instantiation trm and assg :: size 
 begin
@@ -72,12 +48,6 @@
 
 end 
 
-ML {* 
-  val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)}
-*}
-
-
-
 instantiation trm and assg :: pt
 begin
 
@@ -101,13 +71,36 @@
 
 end
 
+ML {*
+  val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct}
+*}
 
-(*
-lemma [quot_respect]:
-  "(alpha_assg_raw ===> alpha_assg_raw ===> op =) alpha_bn_raw alpha_bn_raw"
-apply(simp)
-sorry
-*)
+ML {* 
+  val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.inducts}
+*}
+
+ML {*
+  val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs}
+*}
+
+ML {* 
+  val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)}
+*}
+
+ML {*
+  val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps}
+*}
+
+ML {*
+  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 prod_fv.simps prod_rel.simps prod_alpha_def]}
@@ -134,21 +127,6 @@
 
 section {* NOT *}
 
-
-ML {* 
-  val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)}
-*}
-
-
-ML {*
-  val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps(1)}
-*}
-
-ML {*
-  val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws}
-*}
-
-
 ML {*
   val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps(1)}
 *}