|
1 \usepackage{makeidx} % allows index generation |
|
2 \usepackage{graphicx} % standard LaTeX graphics tool |
|
3 % when including figure files |
|
4 \usepackage{multicol} % used for the two-column index |
|
5 \usepackage[bottom]{footmisc}% places footnotes at page bottom |
|
6 \usepackage{alltt} |
|
7 |
|
8 \usepackage[T1]{fontenc} |
|
9 \usepackage{ccfonts} |
|
10 \usepackage[euler-digits]{eulervm} |
|
11 |
|
12 \let\bfdefaultold=\bfdefault |
|
13 \def\bfdefault{sbc} % make sans serif the default bold font |
|
14 |
|
15 \usepackage{isabelle,isabellesym} |
|
16 \usepackage{mathpartir} |
|
17 \usepackage{amssymb} |
|
18 |
|
19 % Enables fixmes |
|
20 \newif \ifDraft \Drafttrue |
|
21 |
|
22 \ifDraft |
|
23 \newcommand{\FIXME}[1]{\textbf{\textsl{FIXME: #1}}} |
|
24 \else |
|
25 \newcommand{\FIXME}[1]{\relax} |
|
26 \fi |
|
27 |
|
28 \renewcommand*\descriptionlabel[1]{\hspace\labelsep \textbf{#1}\hfil} |
|
29 |
|
30 % this should be the last package used |
|
31 \usepackage{color} |
|
32 \definecolor{linkcolor}{rgb}{0,0,0.4} |
|
33 \usepackage[colorlinks=true,linkcolor=linkcolor,citecolor=linkcolor, |
|
34 filecolor=linkcolor,pagecolor=linkcolor, |
|
35 urlcolor=linkcolor]{hyperref} |
|
36 |
|
37 % urls in roman style, theory text in math-similar italics |
|
38 \urlstyle{tt} |
|
39 \isabellestyle{it} |
|
40 |
|
41 \renewcommand{\isadigit}[1]{\ensuremath{#1}} |
|
42 |
|
43 % font size |
|
44 \renewcommand{\isastyle}{\isastyleminor} |
|
45 |
|
46 % indexing |
|
47 \usepackage{ifthen} |
|
48 \newcommand{\indexdef}[3]% |
|
49 {\ifthenelse{\equal{}{#1}}{\index{#3 (#2)|bold}}{\index{#3 (#1\ #2)|bold}}} |
|
50 |
|
51 % section commands |
|
52 \renewcommand{\chapterautorefname}{Chapter} |
|
53 \renewcommand{\sectionautorefname}{Section} |
|
54 |
|
55 \renewcommand{\isamarkupheader}[1]{{\rmfamily\subsection{#1}}} |
|
56 \renewcommand{\isamarkupsection}[1]{{\rmfamily\subsection{#1}}} |
|
57 \renewcommand{\isamarkupsubsection}[1]{{\rmfamily\subsubsection{#1}}} |
|
58 % isabelle in-text command font |
|
59 \newcommand{\isacom}[1]{\isa{\isacommand{#1}}} |
|
60 % isabelle keyword, adapted from isabelle.sty |
|
61 \renewcommand{\isakeyword}[1] |
|
62 {\emph{\def\isachardot{.}% |
|
63 \def\isacharbraceleft{\{}\def\isacharbraceright{\}}\textbf{#1}}} |
|
64 \renewcommand{\isacharunderscore}{\_} |
|
65 \renewcommand{\isacharunderscorekeyword}{\_} |
|
66 |
|
67 % add \noindent to text blocks automatically |
|
68 \renewenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}} |
|
69 \renewenvironment{isamarkuptxt}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}} |
|
70 |
|
71 \newcommand{\noquotes}[1]{{\renewcommand{\isachardoublequote}{}#1}} |
|
72 \newcommand{\concept}[1]{\textbf{#1}} |
|
73 \newcommand{\xsymbol}[1]{\texttt{\char`\\\char`<#1>}} |
|
74 |
|
75 \newcommand{\isabox}{\fbox} |
|
76 \newcommand{\bigisabox}[1] |
|
77 {\isabox{\renewcommand{\isanewline}{\\}% |
|
78 \begin{tabular}{l}#1\end{tabular}}} |
|
79 |
|
80 %%%% ``WARNING'' environment: 2 ! characters separated by negative thin space |
|
81 %\def\warnbang{\vtop to 0pt{\vss\hbox{\let\bfdefault=\bfdefaultold\Huge\textbf{!$\!$!}}\vss}} |
|
82 |
|
83 \def\warnbang{\vtop to 0pt{\vss\hbox{\includegraphics[width=3ex, height=5.5ex]{bang}}\vss}} |
|
84 |
|
85 \newenvironment{warn}{\begin{trivlist}\small\item[]\noindent% |
|
86 \begingroup\hangindent=\parindent\hangafter=-2%\clubpenalty=10000% |
|
87 \def\par{\endgraf\endgroup}% |
|
88 \hbox to0pt{\hskip-\hangindent\warnbang\hfill}\ignorespaces} |
|
89 {\par\end{trivlist}} |
|
90 |
|
91 \chardef\isachardoublequote=`\"% |
|
92 \chardef\isachardoublequoteopen=`\"% |
|
93 \chardef\isachardoublequoteclose=`\"% |
|
94 |
|
95 \renewcommand{\isacharbackquoteopen}{\isacharbackquote} |
|
96 \renewcommand{\isacharbackquoteclose}{\isacharbackquote} |
|
97 |
|
98 \hyphenation{Isa-belle} |