--- a/Quot/QuotScript.thy	Mon Jan 11 20:04:19 2010 +0100
+++ b/Quot/QuotScript.thy	Mon Jan 11 22:36:21 2010 +0100
@@ -45,11 +45,28 @@
   using a unfolding equivp_def part_equivp_def
   by auto
 
+
+abbreviation 
+  rel_conj (infixr "OOO" 75)
+where
+  "r1 OOO r2 \<equiv> r1 OO r2 OO r1"
+
 definition
   "Quotient E Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and>
                         (\<forall>a. E (Rep a) (Rep a)) \<and>
                         (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
 
+(* TEST
+lemma 
+  fixes Abs1::"'b \<Rightarrow> 'c"
+  and   Abs2::"'a \<Rightarrow> 'b"
+  and   Rep1::"'c \<Rightarrow> 'b"
+  and   Rep2::"'b \<Rightarrow> 'a"
+  assumes "Quotient R1 Abs1 Rep1"
+  and     "Quotient R2 Abs2 Rep2"
+  shows "Quotient (f R2 R1) (Abs1 \<circ> Abs2) (Rep2 \<circ> Rep1)"
+*)
+
 lemma Quotient_abs_rep:
   assumes a: "Quotient E Abs Rep"
   shows "Abs (Rep a) \<equiv> a"
@@ -123,6 +140,7 @@
   shows "(id ---> id) = id"
   by (simp add: expand_fun_eq id_def)
 
+
 fun
   fun_rel
 where
@@ -221,9 +239,10 @@
    will be provable; which is why we need to use apply_rsp and
    not the primed version *)
 lemma apply_rsp:
+  fixes f g::"'a \<Rightarrow> 'c"
   assumes q: "Quotient R1 Abs1 Rep1"
   and     a: "(R1 ===> R2) f g" "R1 x y"
-  shows "R2 ((f::'a\<Rightarrow>'c) x) ((g::'a\<Rightarrow>'c) y)"
+  shows "R2 (f x) (g y)"
   using a by simp
 
 lemma apply_rsp':
@@ -379,8 +398,8 @@
   using Quotient_rel[OF q]
   by metis
 
-(* If a user proves that a particular functional relation is an equivalence
-   this may be useful in regularising *)
+(* If a user proves that a particular functional relation 
+   is an equivalence this may be useful in regularising *)
 lemma babs_reg_eqv:
   shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
   by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp)