|
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 \usepackage{isabelle,isabellesym} |
|
13 \usepackage{mathpartir} |
|
14 \usepackage{amssymb} |
|
15 |
|
16 \renewcommand*\descriptionlabel[1]{\hspace\labelsep \textbf{#1}\hfil} |
|
17 |
|
18 % this should be the last package used |
|
19 \usepackage{xcolor} |
|
20 \definecolor{linkcolor}{rgb}{0,0,0.4} |
|
21 \usepackage[colorlinks=true,linkcolor=linkcolor,citecolor=linkcolor, |
|
22 filecolor=linkcolor,pagecolor=linkcolor, |
|
23 urlcolor=linkcolor]{hyperref} |
|
24 |
|
25 % urls in roman style, theory text in math-similar italics |
|
26 \urlstyle{tt} |
|
27 \isabellestyle{it} |
|
28 |
|
29 \renewcommand{\isadigit}[1]{\ensuremath{#1}} |
|
30 |
|
31 % font size |
|
32 \renewcommand{\isastyle}{\isastyleminor} |
|
33 |
|
34 % indexing |
|
35 \usepackage{ifthen} |
|
36 \newcommand{\indexdef}[3]% |
|
37 {\ifthenelse{\equal{}{#1}}{\index{#3 (#2)|bold}}{\index{#3 (#1\ #2)|bold}}} |
|
38 |
|
39 % section commands |
|
40 \renewcommand{\chapterautorefname}{Chapter} |
|
41 \renewcommand{\sectionautorefname}{Section} |
|
42 \renewcommand{\subsectionautorefname}{Section} |
|
43 |
|
44 \renewcommand{\isamarkupheader}[1]{{\rmfamily\subsection{#1}}} |
|
45 \renewcommand{\isamarkupsection}[1]{{\rmfamily\subsection{#1}}} |
|
46 \renewcommand{\isamarkupsubsection}[1]{{\rmfamily\subsubsection{#1}}} |
|
47 % isabelle in-text command font |
|
48 \newcommand{\isacom}[1]{\isa{\isacommand{#1}}} |
|
49 |
|
50 \protected\def\isacharunderscore{\raisebox{2pt}{\_\kern-1.7pt}} |
|
51 \protected\def\isacharunderscorekeyword{\raisebox{2pt}{\_}} |
|
52 % isabelle keyword, adapted from isabelle.sty |
|
53 \renewcommand{\isakeyword}[1] |
|
54 {\emph{\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}% |
|
55 \def\isacharbraceleft{\{}\def\isacharbraceright{\}}\def\bfdefault{sbc}\textbf{#1}}} |
|
56 |
|
57 % add \noindent to text blocks automatically |
|
58 \renewenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}} |
|
59 \renewenvironment{isamarkuptxt}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}} |
|
60 |
|
61 \newcommand{\noquotes}[1]{{\renewcommand{\isachardoublequote}{}\renewcommand{\isachardoublequoteopen}{}\renewcommand{\isachardoublequoteclose}{}#1}} |
|
62 \newcommand{\xsymbol}[1]{\texttt{\char`\\\char`<#1>}} |
|
63 |
|
64 %index |
|
65 \newcommand{\conceptnoidx}[1]{\textbf{#1}} |
|
66 \newcommand{\concept}[1]{\conceptnoidx{#1}\index{#1}} |
|
67 \newcommand{\conceptidx}[2]{\conceptnoidx{#1}\index{#2}} |
|
68 \newcommand{\indexed}[2]{#1\index{#2@\protect#1}} |
|
69 |
|
70 \newcommand{\isabox}{\fbox} |
|
71 \newcommand{\bigisabox}[1] |
|
72 {\isabox{\renewcommand{\isanewline}{\\}% |
|
73 \begin{tabular}{l}#1\end{tabular}}} |
|
74 |
|
75 %%%% ``WARNING'' environment: 2 ! characters separated by negative thin space |
|
76 %\def\warnbang{\vtop to 0pt{\vss\hbox{\let\bfdefault=\bfdefaultold\Huge\textbf{!$\!$!}}\vss}} |
|
77 |
|
78 \def\warnbang{\vtop to 0pt{\vss\hbox{\includegraphics[width=3ex, height=5.5ex]{bang}}\vss}} |
|
79 |
|
80 \newenvironment{warn}{\begin{trivlist}\small\item[]\noindent% |
|
81 \begingroup\hangindent=\parindent\hangafter=-2%\clubpenalty=10000% |
|
82 \def\par{\endgraf\endgroup}% |
|
83 \hbox to0pt{\hskip-\hangindent\warnbang\hfill}\ignorespaces} |
|
84 {\par\end{trivlist}} |
|
85 |
|
86 \chardef\isachardoublequote=`\"% |
|
87 \chardef\isachardoublequoteopen=`\"% |
|
88 \chardef\isachardoublequoteclose=`\"% |
|
89 |
|
90 \renewcommand{\isacharbackquoteopen}{\isacharbackquote} |
|
91 \renewcommand{\isacharbackquoteclose}{\isacharbackquote} |
|
92 |
|
93 \hyphenation{Isa-belle} |