1 \documentclass[11pt,a4paper]{article} |
1 \documentclass[10pt, conference, compsocconf]{IEEEtran} |
2 \usepackage{isabelle,isabellesym} |
2 \usepackage{isabelle,isabellesym} |
3 %begin adding |
|
4 %\usepackage{pdfsetup} |
|
5 \usepackage{fancyhdr} |
|
6 \usepackage{beamerarticle} |
|
7 \usepackage[english]{babel} |
|
8 %\usepackage{enumitem} |
|
9 \usepackage{enumerate} |
|
10 \usepackage{cases} |
|
11 %\usepackage{CJK,cjknumb} |
|
12 %\usepackage{pgf,pgfarrows,pgfnodes,pgfautomata,pgfheaps,pgfshade} |
|
13 \usepackage{amsmath,amssymb} |
|
14 %\usepackage[latin1]{inputenc} |
|
15 %\usepackage{colortbl} |
|
16 \usepackage{tikz} |
|
17 \usetikzlibrary{arrows,automata,decorations,fit,calc} |
|
18 \usetikzlibrary{shapes,shapes.arrows,snakes,positioning} |
|
19 \usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf |
|
20 \usetikzlibrary{matrix} |
|
21 \usepackage[latin1]{inputenc} |
|
22 \usepackage{verbatim} |
|
23 \usepackage{romannum} |
|
24 \usepackage{makeidx} |
|
25 \usepackage{listings} |
|
26 %end adding |
|
27 % further packages required for unusual symbols (see also |
|
28 % isabellesym.sty), use only when needed |
|
29 |
3 |
30 %\usepackage{amssymb} |
4 %\usepackage{amssymb} |
31 %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>, |
5 %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>, |
32 %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>, |
6 %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>, |
33 %\<triangleq>, \<yen>, \<lozenge> |
7 %\<triangleq>, \<yen>, \<lozenge> |
45 %\usepackage{textcomp} |
19 %\usepackage{textcomp} |
46 %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>, |
20 %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>, |
47 %\<currency> |
21 %\<currency> |
48 |
22 |
49 % this should be the last package used |
23 % this should be the last package used |
|
24 \usepackage{mathpartir} |
50 \usepackage{pdfsetup} |
25 \usepackage{pdfsetup} |
51 |
26 |
52 % urls in roman style, theory text in math-similar italics |
27 % urls in roman style, theory text in math-similar italics |
53 \urlstyle{rm} |
28 \urlstyle{rm} |
54 \isabellestyle{it} |
29 \isabellestyle{it} |
55 |
30 |
56 % for uniform font size |
31 % for uniform font size |
57 %\renewcommand{\isastyle}{\isastyleminor} |
32 %\renewcommand{\isastyle}{\isastyleminor} |
58 \newcommand{\wuhao}{\fontsize{6pt}{10pt}\selectfont} % ÎåºÅ, µ¥±¶Ðоà |
33 |
59 |
34 |
60 \begin{document} |
35 \begin{document} |
61 |
36 |
62 \title{utm} |
37 \title{A Formalised Theorey about Turing Machines in Isablle/HOL} |
63 \author{By xujian} |
38 |
|
39 |
|
40 \author{\IEEEauthorblockN{Authors Name/s per 1st Affiliation (Author)} |
|
41 \IEEEauthorblockA{line 1 (of Affiliation): dept. name of organization\\ |
|
42 line 2: name of organization, acronyms acceptable\\ |
|
43 line 3: City, Country\\ |
|
44 line 4: Email: name@xyz.com} |
|
45 \and |
|
46 \IEEEauthorblockN{Authors Name/s per 2nd Affiliation (Author)} |
|
47 \IEEEauthorblockA{line 1 (of Affiliation): dept. name of organization\\ |
|
48 line 2: name of organization, acronyms acceptable\\ |
|
49 line 3: City, Country\\ |
|
50 line 4: Email: name@xyz.com} |
|
51 } |
|
52 |
64 \maketitle |
53 \maketitle |
65 |
54 |
66 \tableofcontents |
55 |
|
56 \begin{abstract} |
|
57 |
|
58 The abstract goes here. DO NOT USE SPECIAL CHARACTERS, SYMBOLS, OR MATH IN YOUR TITLE OR ABSTRACT. |
|
59 |
|
60 \end{abstract} |
|
61 |
|
62 \begin{IEEEkeywords} |
|
63 Turing Machines, Decidability, Isabelle/HOL; |
|
64 \end{IEEEkeywords} |
|
65 |
|
66 |
|
67 \IEEEpeerreviewmaketitle |
|
68 |
|
69 |
|
70 %\tableofcontents |
67 |
71 |
68 % sane default for proof documents |
72 % sane default for proof documents |
69 \parindent 0pt\parskip 0.5ex |
73 \parindent 0pt\parskip 0.5ex |
|
74 |
|
75 |
|
76 \section{Introduction} |
|
77 |
|
78 text {* |
|
79 |
|
80 |
|
81 *} |
|
82 |
|
83 |
|
84 \noindent |
|
85 {\bf Contributions:} |
|
86 |
70 |
87 |
71 % generated text of all theories |
88 % generated text of all theories |
72 \input{session} |
89 \input{session} |
73 |
90 |
74 % optional bibliography |
91 % optional bibliography |