--- a/Paper/Paper.thy	Wed Jan 26 23:39:42 2011 +0000
+++ b/Paper/Paper.thy	Thu Jan 27 00:51:46 2011 +0000
@@ -1,7 +1,13 @@
 (*<*)
 theory Paper
-imports "../Myhill"
+imports "../Myhill" "LaTeXsugar"
 begin
+
+declare [[show_question_marks = false]]
+
+notation (latex output)
+  str_eq_rel ("\<approx>\<^bsub>_\<^esub>")
+
 (*>*)
 
 section {* Introduction *}
@@ -10,6 +16,34 @@
   
 *}
 
+
+section {* Regular expressions have finitely many partitions *}
+
+text {*
+
+  \begin{lemma}
+  Given @{text "r"} is a regular expressions, then @{thm rexp_imp_finite}.
+  \end{lemma}  
+
+  \begin{proof}
+  By induction on the structure of @{text r}. The cases for @{const NULL}, @{const EMPTY}
+  and @{const CHAR} are starightforward, because we can easily establish
+
+  \begin{center}
+  \begin{tabular}{l}
+  @{thm quot_null_eq}\\
+  @{thm quot_empty_subset}\\
+  @{thm quot_char_subset}
+  \end{tabular}
+  \end{center}
+
+  
+
+  \end{proof}
+
+*}
+
+
 (*<*)
 end
 (*>*)
\ No newline at end of file