# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259239966 -3600
# Node ID 7a1ab11ab02379b2481147e38072ad66124119c2
# Parent  90e58455b2191c9cd0e24ce0086c2bcc7496834c
fixed QuotList

diff -r 90e58455b219 -r 7a1ab11ab023 QuotScript.thy
--- 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)