\documentclass[11pt,a4paper]{article}+
−
\usepackage{isabelle,isabellesym}+
−
\usepackage{amsmath}+
−
\usepackage{amsthm}+
−
\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{subfigure}+
−
+
−
%\usepackage[pdftex]{hyperref}+
−
+
−
% 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[latin1]{inputenc}+
−
  %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,+
−
  %\<threesuperior>, \<threequarters>, \<degree>+
−
+
−
\usepackage{stmaryrd}+
−
  %for \<Sqinter>+
−
+
−
%\usepackage{eufrak}+
−
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)+
−
+
−
%\usepackage{textcomp}+
−
  %for \<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}+
−
+
−
{\theoremstyle{break} \newtheorem{Lem}{Lemma}}+
−
+
−
\newcommand{\dfa}[1]{\hat{\delta}_{#1}}+
−
\newcommand{\Lang}{\mathcal{L}}+
−
\newcommand{\mht}{Myhill-Nerode Theorem}+
−
\newcommand{\qnt}[2]{{#1}//{#2}}+
−
\newcommand{\cls}[2]{\llbracket{#1}\rrbracket_{#2}}+
−
+
−
\begin{document}+
−
+
−
\title{tphols-2011}+
−
\author{By xingyuan}+
−
\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:+
−