--- a/IntEx.thy	Thu Dec 03 11:28:19 2009 +0100
+++ b/IntEx.thy	Thu Dec 03 11:33:24 2009 +0100
@@ -259,12 +259,34 @@
   "(LIST_REL R) [] []"
 by simp
 
+thm LAMBDA_PRS[no_vars]
+thm all_prs[no_vars]
+
+lemma test_all_prs:
+  "\<lbrakk>QUOTIENT R absf repf; f = g\<rbrakk> \<Longrightarrow> Ball (Respects R) ((absf ---> id) f) = All g"
+apply(drule all_prs)
+apply(simp)
+done
+
+lemma test:
+  "\<lbrakk>QUOTIENT R1 Abs1 Rep1; QUOTIENT R2 Abs2 Rep2; 
+    (\<lambda>x. Rep2 (f (Abs1 x))) = lhs \<rbrakk> \<Longrightarrow> (Rep1 ---> Abs2) lhs = f"
+apply -
+thm LAMBDA_PRS
+apply(drule LAMBDA_PRS)
+apply(assumption)
+apply(auto)
+done
+
+
 lemma "foldl PLUS x [] = x"
 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
 apply(simp only: nil_prs)
+apply(rule test_all_prs)
+apply(tactic {* rtac quot 1 *})
 apply(tactic {* clean_tac @{context} [quot] defs 1 *})
 done