--- a/QuotList.thy	Fri Dec 04 09:08:51 2009 +0100
+++ b/QuotList.thy	Fri Dec 04 09:25:27 2009 +0100
@@ -15,7 +15,7 @@
 | "LIST_REL R (x#xs) (y#ys) = (R x y \<and> LIST_REL R xs ys)"
 
 lemma LIST_REL_EQ:
-  shows "LIST_REL (op =) = (op =)"
+  shows "LIST_REL (op =) \<equiv> (op =)"
 unfolding expand_fun_eq
 apply(rule allI)+
 apply(induct_tac x xa rule: list_induct2')