--- a/thys/Journal/Paper.thy	Sun Oct 10 09:56:01 2021 +0100
+++ b/thys/Journal/Paper.thy	Sun Oct 10 18:35:21 2021 +0100
@@ -5,6 +5,7 @@
    "../Simplifying" 
    "../Positions"
    "../Sulzmann"
+(*   "../SizeBound" *)
    "HOL-Library.LaTeXsugar"
 begin
 
@@ -1385,6 +1386,8 @@
 section \<open>Bitcoded Lexing\<close>
 
 
+
+
 text \<open>
 
 Incremental calculation of the value. To simplify the proof we first define the function
@@ -1412,12 +1415,13 @@
   @{term areg} & $::=$ & @{term "AZERO"}\\
                & $\mid$ & @{term "AONE bs"}\\
                & $\mid$ & @{term "ACH bs c"}\\
-               & $\mid$ & @{term "AALT bs r\<^sub>1 r\<^sub>2"}\\
+               & $\mid$ & @{term "AALT bs r1 r2"}\\
                & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\
                & $\mid$ & @{term "ASTAR bs r"}
 \end{tabular}
 \end{center}
 
+
 \begin{center}
   \begin{tabular}{lcl}
   @{thm (lhs) intern.simps(1)} & $\dn$ & @{thm (rhs) intern.simps(1)}\\