--- a/QuotScript.thy	Thu Nov 26 13:46:00 2009 +0100
+++ b/QuotScript.thy	Thu Nov 26 13:52:46 2009 +0100
@@ -468,26 +468,26 @@
   using a b by (metis COMBC_def Collect_def Collect_mem_eq)
 
 lemma LEFT_RES_FORALL_REGULAR:
-  assumes a: "!x. (R x \<and> (Q x --> P x))"
-  shows "Ball R Q --> All P"
+  assumes a: "\<And>x. (R x \<and> (Q x \<longrightarrow> P x))"
+  shows "Ball R Q \<longrightarrow> All P"
   using a
   apply (metis COMBC_def Collect_def Collect_mem_eq a)
   done
 
 lemma RIGHT_RES_FORALL_REGULAR:
-  assumes a: "\<And>x :: 'a. (R x \<Longrightarrow> P x \<longrightarrow> Q x)"
+  assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
   shows "All P \<longrightarrow> Ball R Q"
   using a
   apply (metis COMBC_def Collect_def Collect_mem_eq a)
   done
 
 lemma LEFT_RES_EXISTS_REGULAR:
-  assumes a: "!x :: 'a. (R x \<Longrightarrow> Q x \<longrightarrow> P x)"
+  assumes a: "\<And>x. 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 \<longrightarrow> Q x))"
+  assumes a: "\<And>x. (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)