equal
deleted
inserted
replaced
614 but do not give a formal proof for that in Isabelle/HOL. |
614 but do not give a formal proof for that in Isabelle/HOL. |
615 This is still future work. |
615 This is still future work. |
616 |
616 |
617 |
617 |
618 \section{Structure of the thesis} |
618 \section{Structure of the thesis} |
|
619 \marginpar{\em This is a marginal note.} |
|
620 Before talking about the formal proof of $\blexersimp$'s |
|
621 correctness, which is the main contribution of this thesis, |
|
622 we need to introduce two formal proofs which belong |
|
623 to Ausafe et al. |
619 In chapter \ref{Inj} we will introduce the concepts |
624 In chapter \ref{Inj} we will introduce the concepts |
620 and notations we |
625 and notations we |
621 use for describing regular expressions and derivatives, |
626 use for describing regular expressions and derivatives, |
622 and the first version of Sulzmann and Lu's lexing algorithm without bitcodes (including |
627 and the first version of Sulzmann and Lu's lexing algorithm without bitcodes (including |
623 its correctness proof). |
628 its correctness proof). |