--- a/QuotScript.thy	Fri Dec 04 17:57:03 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 18:32:19 2009 +0100
@@ -43,7 +43,7 @@
 
 lemma Quotient_abs_rep:
   assumes a: "Quotient E Abs Rep"
-  shows "Abs (Rep a) = a"
+  shows "Abs (Rep a) \<equiv> a"
   using a unfolding Quotient_def
   by simp