--- a/ChengsongTanPhdThesis/Chapters/Introduction.tex	Tue Jun 27 01:09:36 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Introduction.tex	Tue Jun 27 16:26:48 2023 +0100
@@ -616,6 +616,11 @@
 
 
 \section{Structure of the thesis}
+\marginpar{\em This is a marginal note.} 
+Before talking about the formal proof of $\blexersimp$'s 
+correctness, which is the main contribution of this thesis,
+we need to introduce two formal proofs which belong
+to Ausafe et al. 
 In chapter \ref{Inj} we will introduce the concepts
 and notations we 
 use for describing regular expressions and derivatives,