# HG changeset patch
# User nipkow
# Date 1101723139 -3600
# Node ID 628d8776743424d0cd1849e3a5ae35562231050a
# Parent  cb35ae957c6516b141e323e39fc3c4ad8d212ab2
New

diff -r cb35ae957c65 -r 628d87767434 doc-src/LaTeXsugar/IsaMakefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/LaTeXsugar/IsaMakefile	Mon Nov 29 11:12:19 2004 +0100
@@ -0,0 +1,31 @@
+
+## targets
+
+default: Sugar
+images: 
+test: Sugar
+
+all: images test
+
+
+## global settings
+
+SRC = $(ISABELLE_HOME)/src
+OUT = $(ISABELLE_OUTPUT)
+LOG = $(OUT)/log
+
+USEDIR = $(ISATOOL) usedir -v true -i true -d pdf -D generated
+
+
+## Sugar
+
+Sugar: $(LOG)/HOL-Sugar.gz
+
+$(LOG)/HOL-Sugar.gz: Sugar/ROOT.ML Sugar/document/root.tex Sugar/*.thy
+	@$(USEDIR) HOL Sugar
+
+
+## clean
+
+clean:
+	@rm -f $(LOG)/HOL-Sugar.gz
diff -r cb35ae957c65 -r 628d87767434 doc-src/LaTeXsugar/Sugar/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/LaTeXsugar/Sugar/ROOT.ML	Mon Nov 29 11:12:19 2004 +0100
@@ -0,0 +1,2 @@
+use_thy "Sugar";
+
diff -r cb35ae957c65 -r 628d87767434 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Mon Nov 29 11:12:19 2004 +0100
@@ -0,0 +1,102 @@
+(*<*)
+theory Sugar
+imports Main
+begin
+(*>*)
+
+section "Introduction"
+
+text{* This document is for those Isabelle users that have mastered
+the art of mixing \LaTeX\ text and Isabelle theories and never want to
+typeset a theorem by hand anymore because they have experienced the
+bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}!
+and seeing Isabelle typeset it for them:
+@{thm[display,eta_contract=false] setsum_cartesian_product[no_vars]}
+No typos, no omissions, no sweat!
+If you have not experienced that joy, read chapter 4, \emph{Presenting
+Theories}, of \cite{LNCS2283} first.
+
+If you have mastered the art of Isabelle's \emph{antiquotations},
+i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
+you may be tempted to think that all readers of the stunning ps or pdf
+documents you can now produce at the drop of a hat will be struck with
+awe at the beauty unfolding in front of their eyes. Until one day you
+come across that very critical of readers known as the ``common referee''.
+He has the nasty habit of refusing to understand unfamiliar notation
+like Isabelle's infamous @{text"\<lbrakk> \<rbrakk> \<Longrightarrow>"} no matter how many times you
+explain it in your paper. Even worse, he thinks that using @{text"\<lbrakk>
+\<rbrakk>"} for anything other than denotational semantics is a cardinal sin
+that must be punished by immediate rejection.
+
+
+This document shows you how to make Isabelle and \LaTeX\ cooperate to
+produce ordinary looking mathematics that hides the fact that it was
+typeset by a machine. This involves additional syntax-related
+declarations for your theory file and corresponding \LaTeX\ macros. We
+explain how to use them but show neither. They can be downloaded from
+the web.
+
+*}
+
+section "Printing theorems"
+
+subsection "Inference rules"
+
+(*<*)
+syntax (Rule output)
+  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>")
+
+  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>")
+
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
+  ("_\<^raw:\\>/ _")
+
+  "_asm" :: "prop \<Rightarrow> asms" ("_")
+(*>*)
+
+text{* To print theorems as inference rules you need to include the
+\texttt{Rule} output syntax declarations in your theory and Didier
+Remy's \texttt{mathpartir} package for typesetting inference rules in
+your \LaTeX\ file.
+
+Writing \verb!@!\verb!{thm[mode=Rule] conjI[no_vars]}! produces
+@{thm[mode=Rule] conjI[no_vars]}, even in the middle of a sentence.
+The standard \texttt{display} attribute, i.e.\ writing
+\verb![mode=Rule,display]! instead of \verb![mode=Rule]!,
+displays the rule on a separate line using a smaller font:
+@{thm[mode=Rule,display] conjI[no_vars]}
+Centering a display does not work directly. Instead you can enclose the
+non-displayed variant in a \texttt{center} environment:
+
+\begin{quote}
+\verb!\begin{center}!\\
+\verb!@!\verb!{thm[mode=Rule] conjI[no_vars]} {\sc conjI}!\\
+\verb!\end{center}!
+\end{quote}
+also adds a label to the rule and yields
+\begin{center}
+@{thm[mode=Rule] conjI[no_vars]} {\sc conjI}
+\end{center}
+Of course you can display multiple rules in this fashion:
+\begin{quote}
+\verb!\begin{center}\isastyle!\\
+\verb!@!\verb!{thm[mode=Rule] conjI[no_vars]} {\sc conjI} \\[1ex]!\\
+\verb!@!\verb!{thm[mode=Rule] conjE[no_vars]} {\sc disjI$_1$} \qquad!\\
+\verb!@!\verb!{thm[mode=Rule] disjE[no_vars]} {\sc disjI$_2$}!\\
+\verb!\end{center}!
+\end{quote}
+yields
+\begin{center}\isastyle
+@{thm[mode=Rule] conjI[no_vars]} {\sc conjI} \\[1ex]
+@{thm[mode=Rule] disjI1[no_vars]} {\sc disjI$_1$} \qquad
+@{thm[mode=Rule] disjI2[no_vars]} {\sc disjI$_2$}
+\end{center}
+Note that we included \verb!\isastyle! to obtain
+the smaller font that otherwise comes only with \texttt{display}.
+
+*}
+(*<*)
+end
+(*>*)
\ No newline at end of file
diff -r cb35ae957c65 -r 628d87767434 doc-src/LaTeXsugar/Sugar/document/mathpartir.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/LaTeXsugar/Sugar/document/mathpartir.sty	Mon Nov 29 11:12:19 2004 +0100
@@ -0,0 +1,354 @@
+%%
+%% This is the original source file mathpar.sty
+%%
+%% Package `mathpar' to use with LaTeX 2e
+%% Copyright Didier Remy, all rights reserved.
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{mathpartir}
+         [2001/23/02 v0.92 Math Paragraph for Type Inference Rules]
+
+%%
+
+%% Identification
+%% Preliminary declarations
+
+\RequirePackage {keyval}
+
+%% Options
+%% More declarations
+
+%% PART I: Typesetting maths in paragraphe mode
+
+\newdimen \mpr@tmpdim
+
+% To ensure hevea \hva compatibility, \hva should expands to nothing 
+% in mathpar or in mathrule
+\let \mpr@hva \empty
+
+%% normal paragraph parametters, should rather be taken dynamically
+\def \mpr@savepar {%
+  \edef \MathparNormalpar
+     {\noexpand \lineskiplimit \the\lineskiplimit
+      \noexpand \lineski \the\lineskip}%
+  }
+
+\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
+\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
+\def \mpr@lineskip  {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
+\let \MathparLineskip \mpr@lineskip
+\def \mpr@paroptions {\MathparLineskip}
+\let \mpr@prebindings \relax
+
+\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
+
+\def \mpr@goodbreakand
+   {\hskip -\mpr@andskip  \penalty -1000\hskip \mpr@andskip}
+\def \mpr@and {\hskip \mpr@andskip}
+\def \mpr@andcr {\penalty 50\mpr@and}
+\def \mpr@cr {\penalty -10000\mpr@and}
+\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
+
+\def \mpr@bindings {%
+  \let \and \mpr@andcr
+  \let \par \mpr@andcr
+  \let \\\mpr@cr
+  \let \eqno \mpr@eqno
+  \let \hva \mpr@hva
+  } 
+\let \MathparBindings \mpr@bindings
+
+\newenvironment{mathpar}[1][]
+  {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
+     \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
+     \noindent $\displaystyle\fi
+     \MathparBindings}
+  {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
+
+% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
+%     \wd0 < \hsize  $$\box0$$\else \bmathpar #1\emathpar \fi}
+
+%%% HOV BOXES
+
+\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip 
+  \vbox \bgroup \tabskip 0em \let \\ \cr
+  \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
+  \egroup}
+
+\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
+      \box0\else \mathvbox {#1}\fi}
+
+
+%% Part II -- operations on lists
+
+\newtoks \mpr@lista
+\newtoks \mpr@listb
+
+\long \def\mpr@cons #1\to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
+
+\long \def\mpr@snoc #1\to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
+
+\long \def \mpr@concat#1=#2\to#3{\mpr@lista \expandafter {#2}\mpr@listb
+\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
+
+\def \mpr@head #1\to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
+\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
+
+\def \mpr@flatten #1\to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
+\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
+
+\def \mpr@makelist #1\to #2{\def \mpr@all {#1}%
+   \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
+   \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty 
+   \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
+     \mpr@flatten \mpr@all \to \mpr@one
+     \expandafter \mpr@snoc \mpr@one \to #2\expandafter \mpr@stripof
+     \mpr@all \mpr@stripend  
+     \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
+     \ifx 1\mpr@isempty
+   \repeat
+}
+
+%% Part III -- Type inference rules
+
+\def \mpr@rev #1\to #2{\let \mpr@tmp \empty
+   \def \\##1{\mpr@cons ##1\to \mpr@tmp}#1\let #2\mpr@tmp}
+
+\newif \if@premisse
+\newbox \mpr@hlist
+\newbox \mpr@vlist
+\newif \ifmpr@center \mpr@centertrue
+\def \mpr@htovlist {%
+   \setbox \mpr@hlist
+      \hbox {\strut
+             \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
+             \unhbox \mpr@hlist}%
+   \setbox \mpr@vlist
+      \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
+             \else \unvbox \mpr@vlist \box \mpr@hlist
+             \fi}%
+}
+% OLD version
+% \def \mpr@htovlist {%
+%    \setbox \mpr@hlist
+%       \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
+%    \setbox \mpr@vlist
+%       \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
+%              \else \unvbox \mpr@vlist \box \mpr@hlist
+%              \fi}%
+% }
+
+
+
+
+\def \mpr@blank { }
+\def \mpr@hovbox #1#2{\hbox
+  \bgroup
+  \ifx #1T\@premissetrue
+  \else \ifx #1B\@premissefalse
+  \else
+     \PackageError{mathpartir}
+       {Premisse orientation should either be P or B}
+       {Fatal error in Package}%
+  \fi \fi
+  \def \@test {#2}\ifx \@test \mpr@blank\else
+  \setbox \mpr@hlist \hbox {}%
+  \setbox \mpr@vlist \vbox {}%
+  \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
+  \let \@hvlist \empty \let \@rev \empty
+  \mpr@tmpdim 0em
+  \expandafter \mpr@makelist #2\to \mpr@flat
+  \if@premisse \mpr@rev \mpr@flat \to \@rev \else \let \@rev \mpr@flat \fi
+  \def \\##1{%
+     \def \@test {##1}\ifx \@test \empty
+        \mpr@htovlist
+        \mpr@tmpdim 0em %%% last bug fix not extensively checked
+     \else
+      \setbox0 \hbox{$\displaystyle {##1}$}\relax
+      \advance \mpr@tmpdim by \wd0
+      %\mpr@tmpdim 1.02\mpr@tmpdim
+      \ifnum \mpr@tmpdim < \hsize
+         \ifnum \wd\mpr@hlist > 0
+           \if@premisse
+             \setbox \mpr@hlist \hbox {\unhbox0 \qquad \unhbox \mpr@hlist}%
+           \else
+             \setbox \mpr@hlist \hbox {\unhbox \mpr@hlist \qquad \unhbox0}%
+           \fi
+         \else 
+         \setbox \mpr@hlist \hbox {\unhbox0}%
+         \fi
+      \else
+         \ifnum \wd \mpr@hlist > 0
+            \mpr@htovlist 
+            \mpr@tmpdim \wd0
+         \fi
+         \setbox \mpr@hlist \hbox {\unhbox0}%
+      \fi
+      \advance \mpr@tmpdim by 2em
+   \fi
+   }%
+   \@rev
+   \mpr@htovlist
+   \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
+   \fi
+   \egroup
+}
+
+%%% INFERENCE RULES
+
+\@ifundefined{@@over}{%
+    \let\@@over\over % fallback if amsmath is not loaded
+    \let\@@overwithdelims\overwithdelims
+    \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
+    \let\@@above\above \let\@@abovewithdelims\abovewithdelims
+  }{}
+
+
+\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
+    $\displaystyle {#1\@@over #2}$}}
+\let \mpr@fraction \mpr@@fraction
+\def \mpr@@reduce #1#2{\hbox
+    {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
+\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
+
+\def \mpr@empty {}
+\def \mpr@inferrule
+  {\bgroup
+     \mpr@rulelineskip
+     \let \and \qquad
+     \let \hva \mpr@hva
+     \let \@rulename \mpr@empty
+     \let \@rule@options \mpr@empty
+     \mpr@inferrule@}
+\newcommand {\mpr@inferrule@}[3][]
+  {\everymath={\displaystyle}%       
+   \def \@test {#2}\ifx \empty \@test
+      \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
+   \else 
+   \def \@test {#3}\ifx \empty \@test
+      \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
+   \else
+   \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
+   \fi \fi
+   \def \@test {#1}\ifx \@test\empty \box0
+   \else \vbox 
+%%% Suggestion de Francois pour les etiquettes longues
+%%%   {\hbox to \wd0 {\TirName {#1}\hfil}\box0}\fi
+      {\hbox {\TirName {#1}}\box0}\fi
+   \egroup}
+
+\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
+
+% They are two forms
+% \mathrule [label]{[premisses}{conclusions}
+% or
+% \mathrule* [options]{[premisses}{conclusions}
+%
+% Premisses and conclusions are lists of elements separated by \\
+% Each \\ produces a break, attempting horizontal breaks if possible, 
+% and  vertical breaks if needed. 
+% 
+% An empty element obtained by \\\\ produces a vertical break in all cases. 
+%
+% The former rule is aligned on the fraction bar. 
+% The optional label appears on top of the rule
+% The second form to be used in a derivation tree is aligned on the last
+% line of its conclusion
+% 
+% The second form can be parameterized, using the key=val interface. The
+% folloiwng keys are recognized:
+%       
+%  width                set the width of the rule to val
+%  narrower             set the width of the rule to val\hsize
+%  before               execute val at the beginning/left
+%  lab                  put a label [Val] on top of the rule
+%  lskip                add negative skip on the right
+%  llab                 put a left label [Val],  ignoring its width 
+%  left                 put a left label [Val]
+%  right                put a right label [Val]
+%  rlab                 put a right label [Val], ignoring its width
+%  rskip                add negative skip on the left
+%  vdots                lift the rule by val and fill vertical space with dots
+%  after                execute val at the end/right
+%  
+%  Note that most options must come in this order to avoid strange
+%  typesetting (in particular  lskip must preceed left and llab and
+%  rskip must follow rlab or right; vdots must come last or be followed by
+%  rskip. 
+%  
+
+\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
+\define@key {mprset}{center}[]{\mpr@centertrue}
+\def \mprset #1{\setkeys{mprset}{#1}}
+
+\newbox \mpr@right
+\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
+\define@key {mpr}{center}[]{\mpr@centertrue}
+\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
+     \advance \hsize by -\wd0\box0}
+\define@key {mpr}{width}{\hsize #1}
+\define@key {mpr}{before}{#1}
+\define@key {mpr}{lab}{\def \mpr@rulename {[#1]}}
+\define@key {mpr}{Lab}{\def \mpr@rulename {#1}}
+\define@key {mpr}{narrower}{\hsize #1\hsize}
+\define@key {mpr}{leftskip}{\hskip -#1}
+\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
+\define@key {mpr}{rightskip}
+  {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
+\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
+     \advance \hsize by -\wd0\box0}
+\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
+\define@key {mpr}{right}
+  {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
+   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{Right}
+  {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
+\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
+\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
+
+\newdimen \rule@dimen
+\newcommand \mpr@inferstar@ [3][]{\setbox0
+  \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
+         \setbox \mpr@right \hbox{}%
+         $\setkeys{mpr}{#1}%
+          \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
+          \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
+          \box \mpr@right \mpr@vdots$}
+  \setbox1 \hbox {\strut}
+  \rule@dimen \dp0 \advance \rule@dimen by -\dp1
+  \raise \rule@dimen \box0}
+
+\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
+\newcommand \mpr@err@skipargs[3][]{}
+\def \mpr@inferstar*{\ifmmode 
+    \let \@do \mpr@inferstar@
+  \else 
+    \let \@do \mpr@err@skipargs
+    \PackageError {mathpartir}
+      {\string\inferrule* can only be used in math mode}{}%
+  \fi \@do}
+
+
+%%% Exports
+
+% Envirnonment mathpar
+
+\let \inferrule \mpr@infer
+
+% make a short name \infer is not already defined
+\@ifundefined {infer}{\let \infer \mpr@infer}{}
+
+\def \tir@name #1{\hbox {\small \sc #1}}
+\let \TirName \tir@name
+
+%%% Other Exports
+
+% \let \listcons \mpr@cons
+% \let \listsnoc \mpr@snoc
+% \let \listhead \mpr@head
+% \let \listmake \mpr@makelist
+
+
+\endinput
+
diff -r cb35ae957c65 -r 628d87767434 doc-src/LaTeXsugar/Sugar/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/LaTeXsugar/Sugar/document/root.tex	Mon Nov 29 11:12:19 2004 +0100
@@ -0,0 +1,59 @@
+\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: