\documentclass[11pt,a4paper]{article}

 \usepackage{isabelle,isabellesym}

 % 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}     % greek for \<euro>,

                                        % english for \<guillemotleft>, 

                                        %             \<guillemotright>

                                        % default language = last

 %\usepackage[latin1]{inputenc}         % for \<onesuperior>, \<onequarter>,

                                        % \<twosuperior>, \<onehalf>,

                                        % \<threesuperior>, \<threequarters>,

                                        % \<degree>

 %\usepackage[only,bigsqcap]{stmaryrd}  % for \<Sqinter>

 %\usepackage{eufrak}                   % for \<AA> ... \<ZZ>, \<aa> ... \<zz>

                                        % (only needed if amssymb not used)

 %\usepackage{textcomp}                 % for \<cent>, \<currency>

 \usepackage{mathpartir}

 % this should be the last package used

 \usepackage{pdfsetup}

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

 \urlstyle{rm}

 \isabellestyle{it}

 \begin{document}

 \title{\LaTeX\ Sugar for Isabelle/HOL}

 \author{Tobias Nipkow, Norbert Schirmer}

 \maketitle

 \begin{abstract}

 This document shows you how to typset mathematics in Isabelle-based

 documents in a style close to that in ordinary computer science papers.

 \end{abstract}

 \tableofcontents

 % generated text of all theories

 \input{session}

 % optional bibliography

 %\bibliographystyle{abbrv}

 %\bibliography{root}

 \end{document}

 %%% Local Variables:

 %%% mode: latex

 %%% TeX-master: t

 %%% End: