diff -r 6fd3fc3254ee -r 53e55a29b788 LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Wed Sep 21 10:23:06 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Wed Sep 21 10:24:01 2011 +0200
@@ -1917,7 +1917,7 @@
   \infer{P}
   {\begin{array}{l}
   @{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. y = C\<AL>\<^isub>1 x\<^isub>1 \<dots> x\<^isub>k \<Rightarrow> P"}\\
-  \hspace{5mm}\ldots\\
+  \hspace{5mm}\vdots\\
   @{text "\<forall>x\<^isub>1\<dots>x\<^isub>l. y = C\<AL>\<^isub>m x\<^isub>1 \<dots> x\<^isub>l \<Rightarrow> P"}\\
   \end{array}}
   \end{equation}\smallskip
@@ -1932,7 +1932,7 @@
   \infer{@{text "P\<^isub>1 y\<^isub>1 \<and> \<dots> \<and> P\<^isub>n y\<^isub>n "}}
   {\begin{array}{l}
   @{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<AL>\<^isub>1 x\<^isub>1 \<dots> x\<^isub>k)"}\\
-  \hspace{5mm}\ldots\\
+  \hspace{5mm}\vdots\\
   @{text "\<forall>x\<^isub>1\<dots>x\<^isub>l. P\<^isub>r x\<^isub>r \<and> \<dots> \<and> P\<^isub>s x\<^isub>s \<Rightarrow> P (C\<AL>\<^isub>m x\<^isub>1 \<dots> x\<^isub>l)"}\\
   \end{array}}
   \end{equation}\smallskip