--- a/QuotScript.thy	Thu Nov 26 12:21:47 2009 +0100
+++ b/QuotScript.thy	Thu Nov 26 13:46:00 2009 +0100
@@ -482,13 +482,13 @@
   done
 
 lemma LEFT_RES_EXISTS_REGULAR:
-  assumes a: "!x :: 'a. (R x --> Q x --> P x)"
-  shows "Bex R Q ==> Ex P"
+  assumes a: "!x :: 'a. (R x \<Longrightarrow> Q x \<longrightarrow> P x)"
+  shows "Bex R Q \<longrightarrow> Ex P"
   using a by (metis COMBC_def Collect_def Collect_mem_eq)
 
 lemma RIGHT_RES_EXISTS_REGULAR:
-  assumes a: "!x :: 'a. (R x \<and> (P x --> Q x))"
-  shows "Ex P \<Longrightarrow> Bex R Q"
+  assumes a: "!x :: 'a. (R x \<and> (P x \<longrightarrow> Q x))"
+  shows "Ex P \<longrightarrow> Bex R Q"
   using a by (metis COMBC_def Collect_def Collect_mem_eq)
 
 (* TODO: Add similar *)