--- a/thys/Paper/Paper.thy	Mon Feb 08 11:54:48 2016 +0000
+++ b/thys/Paper/Paper.thy	Mon Feb 08 15:51:23 2016 +0000
@@ -176,7 +176,7 @@
   @{thm[mode=Rule] PMatch.intros(3)[of "s" "r\<^sub>1" "v" "r\<^sub>2"]}\qquad
   @{thm[mode=Rule] PMatch.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}\medskip\\
   \multicolumn{1}{p{5cm}}{@{thm[mode=Rule] PMatch.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}\medskip\\
-  @{thm[mode=Rule] PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad
+  @{thm[mode=Rule] PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}\medskip\\
   @{thm[mode=Axiom] PMatch.intros(7)}\medskip\\
   \end{tabular}
   \end{center}
@@ -249,6 +249,9 @@
 
   @{thm[mode=IfThen] PMatch1N}
 
+  @{thm[mode=IfThen] PMatch_determ(1)[of "s" "r" "v\<^sub>1" "v\<^sub>2"]}
+
+  \medskip
   \noindent
   This is the main theorem that lets us prove that the algorithm is correct according to
   @{term "s \<in> r \<rightarrow> v"}: