tm: document/root.tex@4b9aa15ff713 (annotated)

1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	1	\documentclass[10pt, conference, compsocconf]{IEEEtran}
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	2	\usepackage{isabelle,isabellesym}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	3
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	4	%\usepackage{amssymb}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	5	%for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	6	%\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	7	%\<triangleq>, \<yen>, \<lozenge>
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	8
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	9	%\usepackage[greek,english]{babel}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	10	%option greek for \<euro>
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	11	%option english (default language) for \<guillemotleft>, \<guillemotright>
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	12
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	13	%\usepackage[only,bigsqcap]{stmaryrd}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	14	%for \<Sqinter>
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	15
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	16	%\usepackage{eufrak}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	17	%for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	18
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	19	%\usepackage{textcomp}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	20	%for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	21	%\<currency>
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	22
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	23	% this should be the last package used
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	24	\usepackage{mathpartir}
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	25	\usepackage{pdfsetup}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	26
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	27	% urls in roman style, theory text in math-similar italics
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	28	\urlstyle{rm}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29	\isabellestyle{it}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	30
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	31	% for uniform font size
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	32	%\renewcommand{\isastyle}{\isastyleminor}
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	33
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	34
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	35	\begin{document}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	36
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	37	\title{A Formalised Theorey about Turing Machines in Isablle/HOL}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	38
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	39
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	40	\author{\IEEEauthorblockN{Authors Name/s per 1st Affiliation (Author)}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	41	\IEEEauthorblockA{line 1 (of Affiliation): dept. name of organization\\
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	42	line 2: name of organization, acronyms acceptable\\
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	43	line 3: City, Country\\
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	44	line 4: Email: name@xyz.com}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	45	\and
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	46	\IEEEauthorblockN{Authors Name/s per 2nd Affiliation (Author)}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	47	\IEEEauthorblockA{line 1 (of Affiliation): dept. name of organization\\
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	48	line 2: name of organization, acronyms acceptable\\
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	49	line 3: City, Country\\
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	50	line 4: Email: name@xyz.com}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	51	}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	52
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	53	\maketitle
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	54
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	55
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	56	\begin{abstract}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	57
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	58	The abstract goes here. DO NOT USE SPECIAL CHARACTERS, SYMBOLS, OR MATH IN YOUR TITLE OR ABSTRACT.
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	59
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	60	\end{abstract}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	61
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	62	\begin{IEEEkeywords}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	63	Turing Machines, Decidability, Isabelle/HOL;
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	64	\end{IEEEkeywords}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	65
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	66
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	67	\IEEEpeerreviewmaketitle
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	68
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	69
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	70	%\tableofcontents
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	71
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	72	% sane default for proof documents
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	73	\parindent 0pt\parskip 0.5ex
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	74
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	75
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	76	\section{Introduction}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	77
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	78	text {*
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	79
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	80
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	81	*}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	82
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	83
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	84	\noindent
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	85	{\bf Contributions:}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	86
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	87
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	88	% generated text of all theories
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	89	\input{session}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	90
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	91	% optional bibliography
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	92	%\bibliographystyle{abbrv}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	93	%\bibliography{root}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	94
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	95	\end{document}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	96
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	97	%%% Local Variables:
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	98	%%% mode: latex
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	99	%%% TeX-master: t
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	100	%%% End:

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Wed, 26 Dec 2012 14:52:14 +0000
changeset 1	4b9aa15ff713
parent 0	aa8656a8dbef
child 2	26b17f2d583e
permissions	-rw-r--r--