--- a/Nominal/Ex/SingleLet.thy	Mon Aug 16 17:39:16 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Mon Aug 16 17:59:09 2010 +0800
@@ -58,47 +58,46 @@
   val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws}
 *}
 
-ML {*
-  Local_Theory.exit_global;
-  Class.instantiation;
-  Class.prove_instantiation_exit_result;
-  Named_Target.theory_init;
-  op |->
-*}
-  
-done
-|> ...
-  |-> (fn x => Class.prove_instantiation_exit_result phi tac x)
-  |-> (fn y => ...)
-
-
 
 section {* NOT *} 
 
+lemma [quot_respect]:
+  "(alpha_assg_raw ===> alpha_assg_raw ===> op =) alpha_bn_raw alpha_bn_raw"
+  "(op = ===> (alpha_trm_raw ===> op =) ===> prod_rel op = alpha_trm_raw ===> op =) prod_fv prod_fv"
+  "((prod_rel op = alpha_trm_raw ===> prod_rel op = alpha_trm_raw ===> op =) ===>
+         (alpha_trm_raw ===> alpha_trm_raw ===> op =) ===>
+            prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw ===>
+            prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw ===> op =)
+            prod_alpha prod_alpha" 
+  "(op = ===>
+         (alpha_trm_raw ===> alpha_trm_raw ===> op =) ===>
+            prod_rel op = alpha_trm_raw ===> prod_rel op = alpha_trm_raw ===> op =)
+            prod_alpha prod_alpha"
+  "((prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw ===>
+             prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw ===> op =) ===>
+            (alpha_trm_raw ===> alpha_trm_raw ===> op =) ===>
+            prod_rel (prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw) alpha_trm_raw ===>
+            prod_rel (prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw) alpha_trm_raw ===>
+            op =)
+            prod_alpha prod_alpha"
+sorry
+
+thm eq_iff(5)
+thm eq_iff(5)[unfolded alphas permute_prod.simps]
+ML {*
+  val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) 
+   @{thms eq_iff(5)[unfolded alphas permute_prod.simps]}
+*}
 
 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]}
 *}
 
 ML {*
-  val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolding alphas]}
+  val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolded alphas]}
 *}
 
 
-(*
-instance trm :: size ..
-instance assg :: size ..
-
-lemma "(size (Var x)) = 0"
-apply(descending)
-apply(rule trm_raw_assg_raw.size(9 - 16))
-apply(simp)
-*)
-
-ML {*
-  val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolding alphas]}
-*}
-
 
 thm perm_defs
 thm perm_simps