diff -r 8b4c8cdd0b51 -r f76c250906d5 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Mon Feb 08 09:56:32 2016 +0000
+++ b/thys/Paper/Paper.thy	Mon Feb 08 11:54:48 2016 +0000
@@ -134,7 +134,7 @@
   @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & 
       @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\
   @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ 
-      & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "c" "v\<^sub>1" "v\<^sub>2"]}\\
+      & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\
   @{thm (lhs) injval.simps(7)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ 
       & @{thm (rhs) injval.simps(7)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\
   @{thm (lhs) injval.simps(8)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ 
@@ -260,6 +260,16 @@
 
 text {*
   \noindent
+  Things we have proved about our version of the Sulzmann ordering
+
+  \begin{center}
+  \begin{tabular}{c}
+  @{thm[mode=IfThen] ValOrd_refl[of "v" "r"]}\medskip\\
+  @{thm[mode=IfThen] ValOrd_total[of "v\<^sub>1" "r" "v\<^sub>2"]}
+  \end{tabular}
+  \end{center}\bigskip  
+
+  \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"}