equal
deleted
inserted
replaced
7 \usepackage{pgf} |
7 \usepackage{pgf} |
8 \usepackage{pdfsetup} |
8 \usepackage{pdfsetup} |
9 \usepackage{ot1patch} |
9 \usepackage{ot1patch} |
10 \usepackage{times} |
10 \usepackage{times} |
11 \usepackage{proof} |
11 \usepackage{proof} |
|
12 %%\usepackage{mathabx} |
12 \usepackage{stmaryrd} |
13 \usepackage{stmaryrd} |
13 \usepackage{mathabx} |
|
14 |
|
15 |
14 |
16 \urlstyle{rm} |
15 \urlstyle{rm} |
17 \isabellestyle{it} |
16 \isabellestyle{it} |
18 \renewcommand{\isastyleminor}{\it}% |
17 \renewcommand{\isastyleminor}{\it}% |
19 \renewcommand{\isastyle}{\normalsize\it}% |
18 \renewcommand{\isastyle}{\normalsize\it}% |
23 \renewcommand{\isasymequiv}{$\dn$} |
22 \renewcommand{\isasymequiv}{$\dn$} |
24 \renewcommand{\isasymemptyset}{$\varnothing$} |
23 \renewcommand{\isasymemptyset}{$\varnothing$} |
25 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
24 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
26 |
25 |
27 \newcommand{\isasymcalL}{\ensuremath{\cal{L}}} |
26 \newcommand{\isasymcalL}{\ensuremath{\cal{L}}} |
|
27 \newcommand{\isasymbigplus}{\ensuremath{\bigplus}} |
|
28 |
|
29 \newcommand{\bigplus}{\mbox{\large\bf$+$}} |
28 \begin{document} |
30 \begin{document} |
29 |
31 |
30 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular |
32 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular |
31 Expressions (Proof Pearl)} |
33 Expressions (Proof Pearl)} |
32 \author{Chunhan Wu\inst{1} \and Xingjuan Zhang\inst{1} \and Christian Urban\inst{2}} |
34 \author{Chunhan Wu\inst{1} \and Xingjuan Zhang\inst{1} \and Christian Urban\inst{2}} |