# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259947939 -3600
# Node ID 8a1f4227dff91a003c17042992ca5f440d871f4b
# Parent  95371a8b17e1ac24c585c1f7b998478f8911544a
abs_rep as ==

diff -r 95371a8b17e1 -r 8a1f4227dff9 QuotScript.thy
--- 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