diff -r 2c56b20032a7 -r 0679a84b11ad prio/document/root.tex
--- a/prio/document/root.tex	Mon Dec 03 08:16:58 2012 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,73 +0,0 @@
-\documentclass[runningheads]{llncs}
-\usepackage{isabelle}
-\usepackage{isabellesym}
-\usepackage{amsmath}
-\usepackage{amssymb}
-\usepackage{tikz}
-\usepackage{pgf}
-\usetikzlibrary{arrows,automata,decorations,fit,calc}
-\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}
-\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf
-\usetikzlibrary{matrix}
-\usepackage{pdfsetup}
-\usepackage{ot1patch}
-\usepackage{times}
-%%\usepackage{proof}
-%%\usepackage{mathabx}
-\usepackage{stmaryrd}
-
-\titlerunning{Proving the Priority Inheritance Protocol Correct}
-
-
-\urlstyle{rm}
-\isabellestyle{it}
-\renewcommand{\isastyleminor}{\it}%
-\renewcommand{\isastyle}{\normalsize\it}%
-
-
-\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
-\renewcommand{\isasymequiv}{$\dn$}
-\renewcommand{\isasymemptyset}{$\varnothing$}
-\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
-
-\newcommand{\isasymcalL}{\ensuremath{\cal{L}}}
-\newcommand{\isasymbigplus}{\ensuremath{\bigplus}}
-
-\newcommand{\bigplus}{\mbox{\Large\bf$+$}}
-\begin{document}
-
-\title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular
-  Expressions (Proof Pearl)}
-\author{Chunhan Wu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}}
-\institute{PLA University of Science and Technology, China \and TU Munich, Germany}
-\maketitle
-
-%\mbox{}\\[-10mm]
-\begin{abstract} 
-There are numerous textbooks on regular languages. Nearly all of them
-introduce the subject by describing finite automata and only mentioning on the
-side a connection with regular expressions. Unfortunately, automata are difficult
-to formalise in HOL-based theorem provers. The reason is that
-they need to be represented as graphs, matrices or functions, none of which
-are inductive datatypes. Also convenient operations for disjoint unions of
-graphs and functions are not easily formalisiable in HOL. In contrast, regular
-expressions can be defined conveniently as a datatype and a corresponding
-reasoning infrastructure comes for free. We show in this paper that a central
-result from formal language theory---the Myhill-Nerode theorem---can be
-recreated using only regular expressions.
-
-\end{abstract}
-
-
-\input{session}
-
-%%\mbox{}\\[-10mm]
-\bibliographystyle{plain}
-\bibliography{root}
-
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End: