--- a/QuotScript.thy	Thu Nov 26 10:52:24 2009 +0100
+++ b/QuotScript.thy	Thu Nov 26 12:21:47 2009 +0100
@@ -469,7 +469,7 @@
 
 lemma LEFT_RES_FORALL_REGULAR:
   assumes a: "!x. (R x \<and> (Q x --> P x))"
-  shows "Ball R Q ==> All P"
+  shows "Ball R Q --> All P"
   using a
   apply (metis COMBC_def Collect_def Collect_mem_eq a)
   done