\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: