diff -r 2a5ac68db24b -r 5347d7556487 Journal/Paper.thy
--- a/Journal/Paper.thy	Thu Aug 11 23:11:39 2011 +0000
+++ b/Journal/Paper.thy	Thu Aug 11 23:42:06 2011 +0000
@@ -617,7 +617,7 @@
   (with the help of a character). In our concrete example we have 
   @{term "X\<^isub>1 \<Turnstile>c\<Rightarrow> X\<^isub>2"}, @{term "X\<^isub>1 \<Turnstile>d\<^isub>i\<Rightarrow> X\<^isub>3"} with @{text "d\<^isub>i"} being any 
   other character than @{text c}, and @{term "X\<^isub>3 \<Turnstile>c\<^isub>j\<Rightarrow> X\<^isub>3"} for any 
-  caracter @{text "c\<^isub>j"}.
+  character @{text "c\<^isub>j"}.
   
   Next we construct an \emph{initial equational system} that
   contains an equation for each equivalence class. We first give
@@ -817,7 +817,7 @@
   
   \noindent
   Our @{text ardenable} condition is slightly stronger than needed for applying Arden's Lemma,
-  but we can still ensure that it holds troughout our algorithm of transforming equations
+  but we can still ensure that it holds throughout our algorithm of transforming equations
   into solved form. The \emph{substitution-operation} takes an equation
   of the form @{text "X = xrhs"} and substitutes it into the right-hand side @{text rhs}.
 
@@ -1557,7 +1557,7 @@
   \end{proof}
 *}
 
-section {* Second Part proved using Partial Derivatives *}
+section {* Second Part proved using Partial Derivatives\label{derivatives} *}
 
 text {*
   \noindent
@@ -1721,7 +1721,7 @@
   Carrying this idea through, we must not consider the set of all derivatives,
   but the ones modulo @{text "ACI"}.  In principle, this can be done formally, 
   but it is very painful in a theorem prover (since there is no
-  direct characterisation of the set of dissimlar derivatives).
+  direct characterisation of the set of dissimilar derivatives).
 
 
   Fortunately, there is a much simpler approach using \emph{partial
@@ -1792,7 +1792,7 @@
   \begin{proof}
   The first fact is by a simple induction on @{text r}. For the second we slightly
   modify Antimirov's proof by performing an induction on @{text s} where we
-  genaralise over all @{text r}. That means in the @{text "cons"}-case the 
+  generalise over all @{text r}. That means in the @{text "cons"}-case the 
   induction hypothesis is
 
   \begin{center}
@@ -2053,7 +2053,9 @@
 
   Our formalisation consists of 780 lines of Isabelle/Isar code for the first
   direction and 460 for the second, plus around 300 lines of standard material
-  about regular languages. While this might be seen large, it should be seen
+  about regular languages. The formalisation about derivatives and partial 
+  derivatives shown in Section~\ref{derivatives} consists of 390 lines of code.
+  While this might be seen large, it should be seen
   in the context of the work done by Constable at al \cite{Constable00} who
   formalised the Myhill-Nerode theorem in Nuprl using automata. They write
   that their four-member team needed something on the magnitude of 18 months
@@ -2068,7 +2070,6 @@
   \mbox{\url{http://www4.in.tum.de/~urbanc/regexp.html}}.
 
 
-
   Our proof of the first direction is very much inspired by \emph{Brzozowski's
   algebraic method} used to convert a finite automaton to a regular
   expression \cite{Brzozowski64}. The close connection can be seen by considering the equivalence