| author | wenzelm | 
| Sun, 02 Oct 2022 16:10:27 +0200 | |
| changeset 76239 | d042947e47a3 | 
| parent 63414 | beb987127d0f | 
| permissions | -rw-r--r-- | 
| 15337 | 1 | \documentclass[11pt,a4paper]{article}
 | 
| 48949 
a773af3e37d6
more standard document preparation within session context;
 wenzelm parents: 
42511diff
changeset | 2 | \usepackage{isabelle,isabellesym}
 | 
| 15337 | 3 | |
| 40729 | 4 | \usepackage{amssymb}
 | 
| 15337 | 5 | |
| 6 | \usepackage{mathpartir}
 | |
| 7 | ||
| 8 | % this should be the last package used | |
| 48949 
a773af3e37d6
more standard document preparation within session context;
 wenzelm parents: 
42511diff
changeset | 9 | \usepackage{pdfsetup}
 | 
| 15337 | 10 | |
| 11 | % urls in roman style, theory text in math-similar italics | |
| 12 | \urlstyle{rm}
 | |
| 13 | \isabellestyle{it}
 | |
| 14 | ||
| 63414 | 15 | \newcommand{\showout}{\mbox{}\hspace{-2em}$\leadsto$\quad}
 | 
| 16 | ||
| 15342 | 17 | \hyphenation{Isa-belle}
 | 
| 15337 | 18 | \begin{document}
 | 
| 19 | ||
| 33323 | 20 | \title{\LaTeX\ Sugar for Isabelle Documents}
 | 
| 15953 | 21 | \author{Florian Haftmann, Gerwin Klein, Tobias Nipkow, Norbert Schirmer}
 | 
| 15337 | 22 | \maketitle | 
| 23 | ||
| 24 | \begin{abstract}
 | |
| 15689 | 25 | This document shows how to typset mathematics in Isabelle-based | 
| 15337 | 26 | documents in a style close to that in ordinary computer science papers. | 
| 27 | \end{abstract}
 | |
| 28 | ||
| 16075 | 29 | %\tableofcontents | 
| 15337 | 30 | |
| 31 | % generated text of all theories | |
| 15342 | 32 | \input{Sugar.tex}
 | 
| 15337 | 33 | |
| 34 | % optional bibliography | |
| 15342 | 35 | \bibliographystyle{abbrv}
 | 
| 36 | \bibliography{root}
 | |
| 15337 | 37 | |
| 38 | \end{document}
 | |
| 39 | ||
| 40 | %%% Local Variables: | |
| 41 | %%% mode: latex | |
| 42 | %%% TeX-master: t | |
| 43 | %%% End: |