--- a/Paper/Paper.thy	Wed Feb 02 13:25:09 2011 +0000
+++ b/Paper/Paper.thy	Wed Feb 02 13:54:07 2011 +0000
@@ -14,16 +14,28 @@
   Seq (infixr "\<cdot>" 100) and
   Star ("_\<^bsup>\<star>\<^esup>") and
   pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and
-  Suc ("_+1>" [100] 100) and
+  Suc ("_+1" [100] 100) and
   quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and
   REL ("\<approx>")
 
-
 (*>*)
 
 section {* Introduction *}
 
 text {*
+  Regular languages are an important and well-understood subject in Computer
+  Science with many beautiful theorems and many useful algorithms. There is a
+  wide range of textbooks about this subject. Many of these textbooks, such as
+  \cite{Kozen97}, are aimed at students and contain very detailed
+  ``pencil-and-paper'' proofs. It seems natural to exercise theorem provers by
+  formalising these theorems and by verifying formally the algorithms. There
+  is however a problem: the typical approach to regular languages is to start
+  with finite automata.
+
+  
+  
+
+
 
   Therefore instead of defining a regular language as being one where there exists an
   automata that regognises all of its strings, we define 
@@ -43,22 +55,26 @@
 section {* Preliminaries *}
 
 text {*
-  Strings in Isabelle/HOL are lists of characters. Therefore the
-  \emph{empty string} is represented by the empty list, written @{term "[]"}. \emph{Languages} are sets of 
-  strings. The language containing all strings is abbreviated as @{term "UNIV::string set"}
-  and the notation for the quotient of a language @{text A} according to a relation @{term REL} is
-  @{term "A // REL"}.
-  
-  Set operations
+  Strings in Isabelle/HOL are lists of characters and the
+  \emph{empty string} is the empty list, written @{term "[]"}. \emph{Languages} are sets of 
+  strings. The language containing all strings is written in Isabelle/HOL as @{term "UNIV::string set"}.
+  The notation for the quotient of a language @{text A} according to a relation @{term REL} is
+  @{term "A // REL"}. The concatenation of two languages is written @{term "A ;; B"}; a language 
+  raised  tow the power $n$ is written @{term "A \<up> n"}. Both concepts are defined as
 
   \begin{center}
-  @{thm Seq_def}
+  @{thm Seq_def[THEN eq_reflection, where A1="A" and B1="B"]}
+  \hspace{7mm}
+  @{thm pow.simps(1)[THEN eq_reflection, where A1="A"]}
+  \hspace{7mm}
+  @{thm pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]}
   \end{center}
 
   \noindent
-  where @{text "@"} is the usual list-append operation.
+  where @{text "@"} is the usual list-append operation. The Kleene-star of a language @{text A}
+  is defined as the union over all powers, namely @{thm Star_def}.
+  
 
-  \noindent
   Regular expressions are defined as the following datatype
 
   \begin{center}