--- a/IntEx.thy	Mon Dec 07 04:39:42 2009 +0100
+++ b/IntEx.thy	Mon Dec 07 04:41:42 2009 +0100
@@ -149,37 +149,6 @@
 apply(rule refl)
 done
 
-
-(*
-lemma yy:
-  "(REP_my_int ---> id)
- (\<lambda>x. Ball (Respects op \<approx>)
-       ((ABS_my_int ---> id)
-         ((REP_my_int ---> id)
-           (\<lambda>b. (ABS_my_int ---> ABS_my_int ---> REP_my_int)
-                 ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus)
-                 (REP_my_int (ABS_my_int x)) (REP_my_int (ABS_my_int b)) \<approx>
-                (ABS_my_int ---> ABS_my_int ---> REP_my_int)
-                 ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus)
-                 (REP_my_int (ABS_my_int x)) (REP_my_int (ABS_my_int b)))))) =
-(\<lambda>x. Ball (Respects op \<approx>)
-     ((ABS_my_int ---> id)
-       ((REP_my_int ---> id)
-         (\<lambda>b. (ABS_my_int ---> ABS_my_int ---> REP_my_int)
-               ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus) (REP_my_int x)
-               (REP_my_int (ABS_my_int b)) \<approx>
-              (ABS_my_int ---> ABS_my_int ---> REP_my_int)
-               ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus) (REP_my_int x)
-               (REP_my_int (ABS_my_int b))))))"
-apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [lambda_prs2 @{theory}]) 1*})
-
-apply(rule lambda_prs)
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(simp add: id_simps)
-apply(tactic {* quotient_tac @{context} 1 *})
-done
-*)
-
 lemma "PLUS a b = PLUS a b"
 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
@@ -187,6 +156,8 @@
 apply(tactic {* clean_tac @{context} 1 *}) 
 done
 
+thm lambda_prs
+
 lemma test2: "my_plus a = my_plus a"
 apply(rule refl)
 done