diff -r 8dbc521ee97f -r 28bb34eeedc5 QuotScript.thy
--- a/QuotScript.thy	Fri Dec 04 09:10:31 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 09:18:46 2009 +0100
@@ -136,7 +136,7 @@
   "E1 ===> E2 \<equiv> FUN_REL E1 E2"
 
 lemma FUN_REL_EQ:
-  "(op =) ===> (op =) = (op =)"
+  "(op =) ===> (op =) \<equiv> (op =)"
 by (simp add: expand_fun_eq)
 
 lemma FUN_QUOTIENT: