| author | wenzelm |
| Fri, 05 Jul 2024 16:28:05 +0200 | |
| changeset 80516 | e7e95718e869 |
| parent 63414 | beb987127d0f |
| permissions | -rw-r--r-- |
| 15337 | 1 |
\documentclass[11pt,a4paper]{article}
|
|
48949
a773af3e37d6
more standard document preparation within session context;
wenzelm
parents:
42511
diff
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:
42511
diff
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: |