Mercurial Mercurial > hg > lexing / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
updated
authorChristian Urban <christian.urban@kcl.ac.uk>
Wed, 23 Mar 2022 00:09:08 +0000
changeset 463 421397f267b9
parent 462 d9b672c4c0ac
child 464 e6248d2c20c2
updated
thys2/Paper/Paper.thy file | annotate | diff | comparison | revisions
thys2/paper.pdf file | annotate | diff | comparison | revisions 
--- 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
Binary file thys2/paper.pdf has changed
lexing