src/ZF/QPair.thy
changeset 13784 b9f6154427a4
parent 13615 449a70d88b38
child 13823 d49ffd9f9662
--- a/src/ZF/QPair.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/QPair.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -283,7 +283,7 @@
         !!x. x: A ==> c(x): C(QInl(x));    
         !!y. y: B ==> d(y): C(QInr(y))  
      |] ==> qcase(c,d,u) : C(u)"
-by (simp add: qsum_defs , auto) 
+by (simp add: qsum_defs, auto) 
 
 (** Rules for the Part primitive **)