\documentclass[11pt,a4paper]{article}+ −
\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>,+ −
%\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,+ −
%\<triangleq>, \<yen>, \<lozenge>+ −
+ −
%\usepackage[greek,english]{babel}+ −
%option greek for \<euro>+ −
%option english (default language) for \<guillemotleft>, \<guillemotright>+ −
+ −
%\usepackage[only,bigsqcap]{stmaryrd}+ −
%for \<Sqinter>+ −
+ −
%\usepackage{eufrak}+ −
%for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)+ −
+ −
%\usepackage{textcomp}+ −
%for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,+ −
%\<currency>+ −
+ −
% this should be the last package used+ −
\usepackage{pdfsetup}+ −
+ −
% urls in roman style, theory text in math-similar italics+ −
\urlstyle{rm}+ −
\isabellestyle{it}+ −
+ −
% for uniform font size+ −
%\renewcommand{\isastyle}{\isastyleminor}+ −
\newcommand{\wuhao}{\fontsize{6pt}{10pt}\selectfont} % ÎåºÅ, µ¥±¶Ðоà+ −
+ −
\begin{document}+ −
+ −
\title{utm}+ −
\author{By xujian}+ −
\maketitle+ −
+ −
\tableofcontents+ −
+ −
% sane default for proof documents+ −
\parindent 0pt\parskip 0.5ex+ −
+ −
% generated text of all theories+ −
\input{session}+ −
+ −
% optional bibliography+ −
%\bibliographystyle{abbrv}+ −
%\bibliography{root}+ −
+ −
\end{document}+ −
+ −
%%% Local Variables:+ −
%%% mode: latex+ −
%%% TeX-master: t+ −
%%% End:+ −