1 \documentclass[11pt,a4paper]{article}

     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 

    30 %\usepackage{amssymb}

    31   %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,

    32   %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,

    33   %\<triangleq>, \<yen>, \<lozenge>

    34 

    35 %\usepackage[greek,english]{babel}

    36   %option greek for \<euro>

    37   %option english (default language) for \<guillemotleft>, \<guillemotright>

    38 

    39 %\usepackage[only,bigsqcap]{stmaryrd}

    40   %for \<Sqinter>

    41 

    42 %\usepackage{eufrak}

    43   %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)

    44 

    45 %\usepackage{textcomp}

    46   %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,

    47   %\<currency>

    48 

    49 % this should be the last package used

    50 \usepackage{pdfsetup}

    51 

    52 % urls in roman style, theory text in math-similar italics

    53 \urlstyle{rm}

    54 \isabellestyle{it}

    55 

    56 % for uniform font size

    57 %\renewcommand{\isastyle}{\isastyleminor}

    58 \newcommand{\wuhao}{\fontsize{6pt}{10pt}\selectfont}    % ÎåºÅ, µ¥±¶Ðоà

    59 

    60 \begin{document}

    61 

    62 \title{utm}

    63 \author{By xujian}

    64 \maketitle

    65 

    66 \tableofcontents

    67 

    68 % sane default for proof documents

    69 \parindent 0pt\parskip 0.5ex

    70 

    71 % generated text of all theories

    72 \input{session}

    73 

    74 % optional bibliography

    75 %\bibliographystyle{abbrv}

    76 %\bibliography{root}

    77 

    78 \end{document}

    79 

    80 %%% Local Variables:

    81 %%% mode: latex

    82 %%% TeX-master: t

    83 %%% End: