diff -r 38696f516c6b -r 8b4c8cdd0b51 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Sun Feb 07 23:44:34 2016 +0000
+++ b/thys/Paper/Paper.thy	Mon Feb 08 09:56:32 2016 +0000
@@ -201,18 +201,69 @@
   @{thm[mode=Axiom] ValOrd.intros(13)[of "r"]}\medskip\\
   \end{tabular}
   \end{center}
+
+  \noindent
+  A prefix of a string s
+
+  \begin{center}
+  \begin{tabular}{c}
+  @{thm prefix_def[of "s\<^sub>1" "s\<^sub>2"]}
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  Values and non-problematic values
+
+  \begin{center}
+  \begin{tabular}{c}
+  @{thm Values_def}\medskip\\
+  @{thm NValues_def}
+  \end{tabular}
+  \end{center}
+
+
+  \noindent
+  The point is that for a given @{text s} and @{text r} there are only finitely many
+  non-problematic values.
 *} 
 
 text {* 
   \noindent
-  Some lemmas
+  Some lemmas we have proved:\bigskip
   
+  @{thm L_flat_Prf}
+
+  @{thm L_flat_NPrf}
 
   @{thm[mode=IfThen] mkeps_nullable}
 
   @{thm[mode=IfThen] mkeps_flat}
 
-  \ldots
+  @{thm[mode=IfThen] v3}
+
+  @{thm[mode=IfThen] v4}
+  
+  @{thm[mode=IfThen] PMatch_mkeps}
+  
+  @{thm[mode=IfThen] PMatch1(2)}
+
+  @{thm[mode=IfThen] PMatch1N}
+
+  \noindent
+  This is the main theorem that lets us prove that the algorithm is correct according to
+  @{term "s \<in> r \<rightarrow> v"}:
+
+  @{thm[mode=IfThen] PMatch2}
+
+  \mbox{}\bigskip
+*}
+
+text {*
+  \noindent
+  Things we like to prove, but cannot:\bigskip
+
+  If @{term "s \<in> r \<rightarrow> v\<^sub>1"}, @{term "\<turnstile> v\<^sub>2 : r"}, then @{term "v\<^sub>1 \<succ>r v\<^sub>2"}
+  
 *}