# HG changeset patch
# User kleing
# Date 1140385218 -3600
# Node ID 9804aa8d5756c1354cd0f0e79d0277bdb369deb3
# Parent  6f8c1343341bd96288c4e87536e48f34a4b65319
fixed document

diff -r 6f8c1343341b -r 9804aa8d5756 src/HOL/Complex/ex/ROOT.ML
--- a/src/HOL/Complex/ex/ROOT.ML	Sun Feb 19 22:12:30 2006 +0100
+++ b/src/HOL/Complex/ex/ROOT.ML	Sun Feb 19 22:40:18 2006 +0100
@@ -15,6 +15,9 @@
 no_document use_thy "BigO";
 use_thy "BigO_Complex";
 
+no_document use_thy "ASeries";
 use_thy "ASeries_Complex";
 use_thy "HarmonicSeries";
+
+no_document use_thy "NatPair";
 use_thy "DenumRat";
diff -r 6f8c1343341b -r 9804aa8d5756 src/HOL/Library/ASeries.thy
--- a/src/HOL/Library/ASeries.thy	Sun Feb 19 22:12:30 2006 +0100
+++ b/src/HOL/Library/ASeries.thy	Sun Feb 19 22:40:18 2006 +0100
@@ -24,14 +24,14 @@
 "http://mathworld.wolfram.com/ArithmeticSeries.html")
   The proof is a simple forward proof. Let $S$ equal the sum above and
   $a$ the first element, then we have
-\begin{align}
-\nonumber  S &= a + (a+d) + (a+2d) + ... a_n \\
-\nonumber    &= n*a + d (0 + 1 + 2 + ... n-1) \\
-\nonumber    &= n*a + d (\frac{1}{2} * (n-1) * n)    \mbox{..using a simple sum identity} \\
-\nonumber    &= \frac{n}{2} (2a + d(n-1)) \\
-\nonumber    & \mbox{..but $(a+a_n = a + (a + d(n-1)) = 2a + d(n-1))$ so} \\
-\nonumber  S &= \frac{n}{2} (a + a_n)
-\end{align}
+\begin{tabular}{ll}
+  $S$ &$= a + (a+d) + (a+2d) + ... a_n$ \\
+    &$= n*a + d (0 + 1 + 2 + ... n-1)$ \\
+    &$= n*a + d (\frac{1}{2} * (n-1) * n)$   ..using a simple sum identity \\
+    &$= \frac{n}{2} (2a + d(n-1))$ \\
+    & ..but $(a+a_n = a + (a + d(n-1)) = 2a + d(n-1))$ so \\
+  $S$ &$= \frac{n}{2} (a + a_n)$
+\end{tabular}
 *}
 
 section {* Formal Proof *}