--- a/thys/Paper/Paper.thy	Mon Feb 08 15:51:23 2016 +0000
+++ b/thys/Paper/Paper.thy	Wed Feb 10 17:38:29 2016 +0000
@@ -127,20 +127,18 @@
   \begin{center}
   \begin{tabular}{lcl}
   @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\
-  @{thm (lhs) injval.simps(2)} & $\dn$ & @{thm (rhs) injval.simps(2)}\\
-  @{thm (lhs) injval.simps(3)} & $\dn$ & @{thm (rhs) injval.simps(3)}\\
-  @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & 
-      @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\
-  @{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" "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$ 
-      & @{thm (rhs) injval.simps(8)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\
-  @{thm (lhs) injval.simps(9)[of "r" "c" "v" "vs"]} & $\dn$ 
-      & @{thm (rhs) injval.simps(9)[of "r" "c" "v" "vs"]}\\
+  @{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & 
+      @{thm (rhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\
+  @{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & 
+      @{thm (rhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\
+  @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ 
+      & @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\
+  @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ 
+      & @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\
+  @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ 
+      & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\
+  @{thm (lhs) injval.simps(7)[of "r" "c" "v" "vs"]} & $\dn$ 
+      & @{thm (rhs) injval.simps(7)[of "r" "c" "v" "vs"]}\\
   \end{tabular}
   \end{center}
 
@@ -268,7 +266,7 @@
   \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"]}
+  %@ {thm[mode=IfThen] ValOrd_total[of "v\<^sub>1" "r" "v\<^sub>2"]}
   \end{tabular}
   \end{center}\bigskip  
 
@@ -288,6 +286,42 @@
 
   \bibliographystyle{plain}
   \bibliography{root}
+
+  \section{Roy's Rules}
+
+   \newcommand{\abs}[1]{\mid\!\! #1\!\! \mid}
+   %%\newcommand{\mts}{\textit{``''}
+   \newcommand{\tl}{\ \triangleleft\ }
+   $$\inferrule[]{Void \tl \epsilon}{}
+            \quad\quad
+     \inferrule[]{Char\ c \tl Lit\ c}{}
+   $$
+   $$\inferrule
+       {v_1 \tl r_1}
+       {Left\ v_1 \tl r_1 + r_2}
+   \quad\quad
+     \inferrule[]
+       { v_2 \tl r_2 \\ \abs{v_2}\ \not\in\ L(r_1)}
+       {Right\ v_2 \tl r_1 + r_2}
+   $$
+   $$
+   \inferrule
+       {v_1 \tl r_1\\
+        v_2 \tl r_2\\
+        s \in\  L(r_1\backslash\! \abs{v_1}) \ \land\
+        \abs{v_2}\!\backslash s\ \epsilon\ L(r_2)
+        \ \Rightarrow\ s = []
+       }
+       {(v_1, v_2) \tl r_1 \cdot r_2}
+   $$
+   $$\inferrule
+         { v \tl r \\ vs \tl r^* \\ \abs{v}\ \not=\ []} 
+         { (v :: vs) \tl r^* }
+   \quad\quad
+       \inferrule{}
+         { []  \tl r^* }       
+   $$
+
 *}