diff -r aa8656a8dbef -r 4b9aa15ff713 document/root.tex
--- a/document/root.tex	Mon Dec 24 01:26:23 2012 +0000
+++ b/document/root.tex	Wed Dec 26 14:52:14 2012 +0000
@@ -1,31 +1,5 @@
-\documentclass[11pt,a4paper]{article}
+\documentclass[10pt, conference, compsocconf]{IEEEtran}
 \usepackage{isabelle,isabellesym}
-%begin adding
-%\usepackage{pdfsetup}
-\usepackage{fancyhdr}
-\usepackage{beamerarticle}
-\usepackage[english]{babel}
-%\usepackage{enumitem}
-\usepackage{enumerate}
-\usepackage{cases}
-%\usepackage{CJK,cjknumb}
-%\usepackage{pgf,pgfarrows,pgfnodes,pgfautomata,pgfheaps,pgfshade}
-\usepackage{amsmath,amssymb}
-%\usepackage[latin1]{inputenc}
-%\usepackage{colortbl}
-\usepackage{tikz}
-\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[latin1]{inputenc}
-\usepackage{verbatim}
-\usepackage{romannum}
-\usepackage{makeidx}
-\usepackage{listings}
-%end adding
-% further packages required for unusual symbols (see also
-% isabellesym.sty), use only when needed
 
 %\usepackage{amssymb}
   %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
@@ -47,6 +21,7 @@
   %\<currency>
 
 % this should be the last package used
+\usepackage{mathpartir}
 \usepackage{pdfsetup}
 
 % urls in roman style, theory text in math-similar italics
@@ -55,19 +30,61 @@
 
 % for uniform font size
 %\renewcommand{\isastyle}{\isastyleminor}
-\newcommand{\wuhao}{\fontsize{6pt}{10pt}\selectfont}    % ÎåºÅ, µ¥±¶Ðоà
+
 
 \begin{document}
 
-\title{utm}
-\author{By xujian}
+\title{A Formalised Theorey about Turing Machines in Isablle/HOL}
+
+
+\author{\IEEEauthorblockN{Authors Name/s per 1st Affiliation (Author)}
+\IEEEauthorblockA{line 1 (of Affiliation): dept. name of organization\\
+line 2: name of organization, acronyms acceptable\\
+line 3: City, Country\\
+line 4: Email: name@xyz.com}
+\and
+\IEEEauthorblockN{Authors Name/s per 2nd Affiliation (Author)}
+\IEEEauthorblockA{line 1 (of Affiliation): dept. name of organization\\
+line 2: name of organization, acronyms acceptable\\
+line 3: City, Country\\
+line 4: Email: name@xyz.com}
+}
+
 \maketitle
 
-\tableofcontents
+
+\begin{abstract}
+
+The abstract goes here. DO NOT USE SPECIAL CHARACTERS, SYMBOLS, OR MATH IN YOUR TITLE OR ABSTRACT.
+
+\end{abstract}
+
+\begin{IEEEkeywords}
+Turing Machines, Decidability, Isabelle/HOL;
+\end{IEEEkeywords}
+
+
+\IEEEpeerreviewmaketitle
+
+
+%\tableofcontents
 
 % sane default for proof documents
 \parindent 0pt\parskip 0.5ex
 
+
+\section{Introduction}
+
+text {*
+  
+
+*}
+
+
+\noindent
+{\bf Contributions:} 
+
+
 % generated text of all theories
 \input{session}