diff -r d9b672c4c0ac -r 421397f267b9 thys2/Paper/Paper.thy
--- a/thys2/Paper/Paper.thy	Tue Mar 22 11:14:02 2022 +0000
+++ b/thys2/Paper/Paper.thy	Wed Mar 23 00:09:08 2022 +0000
@@ -968,8 +968,8 @@
      %
      \begin{equation}\label{derivex}
      (a + aa)^* \quad\xll\quad
-      \underbrace{\mbox{$(\ONE + \ONE{}a) \cdot (a + aa)^*$}}_{r} \;+\;
-     ((a + aa)^* + \underbrace{\mbox{$(\ONE + \ONE{}a) \cdot (a + aa)^*$}}_{r})
+      \underbrace{\mbox{$(\ONE + a) \cdot (a + aa)^*$}}_{r} \;+\;
+     ((a + aa)^* + \underbrace{\mbox{$(\ONE + a) \cdot (a + aa)^*$}}_{r})
      \end{equation}
 
      \noindent This is a simpler derivative, but unfortunately we