
diff -r eed5d55ea9a6 -r 6b3be083229c QuotScript.thy
--- a/QuotScript.thy	Fri Dec 04 09:08:51 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 09:25:27 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:




