--- a/document/root.tex	Thu Jan 17 11:51:00 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,62 +0,0 @@
-\documentclass[runningheads]{llncs}
-%\documentclass[10pt, conference, compsocconf]{IEEEtran}
-\usepackage{isabelle}
-\usepackage{isabellesym}
-\usepackage{times}
-\usepackage{amssymb}
-\usepackage{amsmath}
-\usepackage{mathpartir}
-\usepackage{pdfsetup}
-\usepackage{tikz}
-\usepackage{pgf}
-
-% urls in roman style, theory text in math-similar italics
-\urlstyle{rm}
-\isabellestyle{it}
-
-% for uniform font size
-%\renewcommand{\isastyle}{\isastyleminor}
-
-\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
-\renewcommand{\isasymequiv}{$\dn$}
-\renewcommand{\isasymemptyset}{$\varnothing$}
-\renewcommand{\isacharunderscore}{\mbox{$\_$}}
-\renewcommand{\isasymiota}{}
-\newcommand{\isasymulcorner}{$\ulcorner$}
-\newcommand{\isasymurcorner}{$\urcorner$}
-\begin{document}
-
-
-\title{Formalising Computability Theory in Isabelle/HOL}
-\author{Jian Xu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}}
-\institute{PLA University of Science and Technology, China \and King's College London, UK}
-
-\maketitle
-
-
-\begin{abstract}
-We present a formalised theory of computability in the 
-theorem prover Isabelle/HOL. This theorem prover is based on classical 
-logic which precludes \emph{direct} reasoning about computability: every 
-boolean predicate is either true or false because of the law of excluded 
-middle. The only way to reason about computability in a classical theorem 
-prover is to formalise a concrete model for computation. 
-We formalise Turing machines and relate them to abacus machines and recursive
-functions. Our theory can be used to formalise other computability results:
-we give one example about the undecidability of Wang's tiling problem, whose proof uses
-the notion of a universal Turing machine.
-\end{abstract}
-
-% generated text of all theories
-\input{session}
-
-% optional bibliography
-\bibliographystyle{abbrv}
-\bibliography{root}
-
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End: