--- a/IntEx.thy	Mon Dec 07 12:14:25 2009 +0100
+++ b/IntEx.thy	Mon Dec 07 14:00:36 2009 +0100
@@ -246,27 +246,31 @@
 
 lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *})
-(*apply(tactic {* regularize_tac @{context} 1 *}) *)
-defer
+apply(tactic {* regularize_tac @{context} 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 apply(simp add: pair_prs)
-sorry
+done
 
 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
 by simp
 
+
+
+
 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
-apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
-apply(tactic {* gen_frees_tac @{context} 1 *})
-ML_prf {* regularize_trm @{context} (prop_of @{thm lam_tst2}) @{prop "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"} *}
-ML_prf {* print_depth 50 *}
-ML_prf {* Syntax.check_term @{context} it *}
-ML_prf {* procedure_inst @{context} (prop_of @{thm lam_tst2}) @{prop "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"} *}
+apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *})
+defer
+apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+(*apply(tactic {* lambda_prs_tac  @{context} 1 *})*)
+sorry
 
-apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
+lemma lam_tst3: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"
+by auto
+
+lemma "(\<lambda>(y :: my_int \<Rightarrow> my_int). y) = (\<lambda>(x :: my_int \<Rightarrow> my_int). x)"
+apply(tactic {* procedure_tac @{context} @{thm lam_tst3} 1 *})
+defer
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* clean_tac @{context} 1 *})
-done
-
+apply(tactic {* lambda_prs_tac  @{context} 1 *})
+sorry