tm: document/root.tex@aa8656a8dbef (annotated)

0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1	\documentclass[11pt,a4paper]{article}
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	%begin adding
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	4	%\usepackage{pdfsetup}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	5	\usepackage{fancyhdr}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	6	\usepackage{beamerarticle}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	7	\usepackage[english]{babel}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	8	%\usepackage{enumitem}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	9	\usepackage{enumerate}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	10	\usepackage{cases}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	11	%\usepackage{CJK,cjknumb}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	12	%\usepackage{pgf,pgfarrows,pgfnodes,pgfautomata,pgfheaps,pgfshade}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	13	\usepackage{amsmath,amssymb}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	14	%\usepackage[latin1]{inputenc}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	15	%\usepackage{colortbl}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	16	\usepackage{tikz}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	17	\usetikzlibrary{arrows,automata,decorations,fit,calc}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	18	\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	19	\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	20	\usetikzlibrary{matrix}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	21	\usepackage[latin1]{inputenc}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	22	\usepackage{verbatim}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	23	\usepackage{romannum}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	24	\usepackage{makeidx}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	25	\usepackage{listings}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	26	%end adding
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	27	% further packages required for unusual symbols (see also
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	28	% isabellesym.sty), use only when needed
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	30	%\usepackage{amssymb}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	31	%for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	32	%\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	33	%\<triangleq>, \<yen>, \<lozenge>
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	%\usepackage[greek,english]{babel}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	36	%option greek for \<euro>
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	37	%option english (default language) for \<guillemotleft>, \<guillemotright>
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	38
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	39	%\usepackage[only,bigsqcap]{stmaryrd}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	40	%for \<Sqinter>
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	41
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	42	%\usepackage{eufrak}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	43	%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	44
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	45	%\usepackage{textcomp}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	46	%for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	47	%\<currency>
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	48
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	49	% this should be the last package used
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	50	\usepackage{pdfsetup}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	51
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	52	% 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	53	\urlstyle{rm}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	54	\isabellestyle{it}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	55
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	56	% for uniform font size
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	57	%\renewcommand{\isastyle}{\isastyleminor}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	58	\newcommand{\wuhao}{\fontsize{6pt}{10pt}\selectfont} % ÎåºÅ, µ¥±¶ÐÐ¾à
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	59
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	60	\begin{document}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	61
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	62	\title{utm}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	63	\author{By xujian}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	64	\maketitle
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	65
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	66	\tableofcontents
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	67
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	68	% sane default for proof documents
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	69	\parindent 0pt\parskip 0.5ex
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	70
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	71	% generated text of all theories
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	72	\input{session}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	73
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	74	% optional bibliography
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	75	%\bibliographystyle{abbrv}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	76	%\bibliography{root}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	77
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	78	\end{document}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	79
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	80	%%% Local Variables:
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	81	%%% mode: latex
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	82	%%% TeX-master: t
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	83	%%% End:

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Mon, 24 Dec 2012 01:26:23 +0000
changeset 0	aa8656a8dbef
child 1	4b9aa15ff713
permissions	-rw-r--r--