--- a/IntEx.thy	Sun Dec 06 02:41:35 2009 +0100
+++ b/IntEx.thy	Sun Dec 06 04:03:08 2009 +0100
@@ -147,15 +147,37 @@
 apply(rule refl)
 done
 
-abbreviation 
-  "Abs \<equiv> ABS_my_int"
-abbreviation 
-  "Rep \<equiv> REP_my_int"
-abbreviation 
-  "Resp \<equiv> Respects"
 
-thm apply_rsp rep_abs_rsp lambda_prs
-ML {* map (Pattern.pattern o bare_concl o prop_of) @{thms apply_rsp rep_abs_rsp lambda_prs} *}
+(*
+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"