# HG changeset patch
# User Christian Urban <christian.urban@kcl.ac.uk>
# Date 1651579901 -3600
# Node ID 1ab693d6342f42bdf27f840e5fa5ffdd53878835
# Parent  a6d72af04096368d5d876dac7a44734c4f350793
fixed a small typo in the Papaer.thy

diff -r a6d72af04096 -r 1ab693d6342f thys3/Paper.thy
--- a/thys3/Paper.thy	Mon May 02 00:24:01 2022 +0100
+++ b/thys3/Paper.thy	Tue May 03 13:11:41 2022 +0100
@@ -1353,7 +1353,7 @@
 % tell Chengsong about Indian paper of closed forms of derivatives
 
 \noindent
-where in (1) the $\textit{Suffix}(@{text "r"}_1, s)$ are the all the suffixes of $s$ where @{term "bders_simp r\<^sub>1 s'"} is nullable ($s'$ being a suffix of $s$).
+where in (1) the $\textit{Suffix}(@{text "r"}_1, s)$ are all the suffixes of $s$ where @{term "bders_simp r\<^sub>1 s'"} is nullable ($s'$ being a suffix of $s$).
 In (3) we know that  $\llbracket@{term "ASEQ [] (bders_simp r\<^sub>1 s) r\<^sub>2"}\rrbracket$ is 
 bounded by $N_1 + \llbracket{}r_2\rrbracket + 1$. In (5) we know the list comprehension contains only regular expressions of size smaller
 than $N_2$. The list length after @{text distinctWith} is bounded by a number, which we call $l_{N_2}$. It stands