|
1 \documentclass[11pt,a4paper]{article} |
|
2 \usepackage{isabelle,isabellesym} |
|
3 |
|
4 % further packages required for unusual symbols (see also isabellesym.sty) |
|
5 % use only when needed |
|
6 %\usepackage{amssymb} % for \<leadsto>, \<box>, \<diamond>, |
|
7 % \<sqsupset>, \<mho>, \<Join>, |
|
8 % \<lhd>, \<lesssim>, \<greatersim>, |
|
9 % \<lessapprox>, \<greaterapprox>, |
|
10 % \<triangleq>, \<yen>, \<lozenge> |
|
11 %\usepackage[greek,english]{babel} % greek for \<euro>, |
|
12 % english for \<guillemotleft>, |
|
13 % \<guillemotright> |
|
14 % default language = last |
|
15 %\usepackage[latin1]{inputenc} % for \<onesuperior>, \<onequarter>, |
|
16 % \<twosuperior>, \<onehalf>, |
|
17 % \<threesuperior>, \<threequarters>, |
|
18 % \<degree> |
|
19 %\usepackage[only,bigsqcap]{stmaryrd} % for \<Sqinter> |
|
20 %\usepackage{eufrak} % for \<AA> ... \<ZZ>, \<aa> ... \<zz> |
|
21 % (only needed if amssymb not used) |
|
22 %\usepackage{textcomp} % for \<cent>, \<currency> |
|
23 |
|
24 \usepackage{mathpartir} |
|
25 |
|
26 % this should be the last package used |
|
27 \usepackage{pdfsetup} |
|
28 |
|
29 % urls in roman style, theory text in math-similar italics |
|
30 \urlstyle{rm} |
|
31 \isabellestyle{it} |
|
32 |
|
33 \hyphenation{Isa-belle} |
|
34 \begin{document} |
|
35 |
|
36 \title{\LaTeX\ Sugar for Isabelle documents} |
|
37 \author{Gerwin Klein, Tobias Nipkow, Norbert Schirmer} |
|
38 \maketitle |
|
39 |
|
40 \begin{abstract} |
|
41 This document shows how to typset mathematics in Isabelle-based |
|
42 documents in a style close to that in ordinary computer science papers. |
|
43 \end{abstract} |
|
44 |
|
45 \tableofcontents |
|
46 |
|
47 % generated text of all theories |
|
48 \input{Sugar.tex} |
|
49 |
|
50 % optional bibliography |
|
51 \bibliographystyle{abbrv} |
|
52 \bibliography{root} |
|
53 |
|
54 \end{document} |
|
55 |
|
56 %%% Local Variables: |
|
57 %%% mode: latex |
|
58 %%% TeX-master: t |
|
59 %%% End: |