56820
|
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 |
|
|
10 |
\usepackage{isabelle,isabellesym}
|
|
11 |
%\usepackage{amssymb}
|
|
12 |
|
|
13 |
\renewcommand*\descriptionlabel[1]{\hspace\labelsep \textbf{#1}\hfil}
|
|
14 |
|
|
15 |
% this should be the last package used
|
|
16 |
\usepackage{xcolor}
|
|
17 |
\definecolor{linkcolor}{rgb}{0,0,0.4}
|
|
18 |
\usepackage[colorlinks=true,linkcolor=linkcolor,citecolor=linkcolor,
|
|
19 |
filecolor=linkcolor,pagecolor=linkcolor,
|
|
20 |
urlcolor=linkcolor]{hyperref}
|
|
21 |
|
|
22 |
% urls in roman style, theory text in math-similar italics
|
|
23 |
\urlstyle{tt}
|
|
24 |
\isabellestyle{it}
|
|
25 |
|
|
26 |
\renewcommand{\isadigit}[1]{\ensuremath{#1}}
|
|
27 |
|
|
28 |
% font size
|
|
29 |
\renewcommand{\isastyle}{\isastyleminor}
|
|
30 |
|
|
31 |
% indexing
|
|
32 |
\usepackage{ifthen}
|
|
33 |
\newcommand{\indexdef}[3]%
|
|
34 |
{\ifthenelse{\equal{}{#1}}{\index{#3 (#2)|bold}}{\index{#3 (#1\ #2)|bold}}}
|
|
35 |
|
|
36 |
\renewcommand{\isamarkupheader}[1]{{\rmfamily\subsection{#1}}}
|
|
37 |
\renewcommand{\isamarkupsection}[1]{{\rmfamily\subsection{#1}}}
|
|
38 |
\renewcommand{\isamarkupsubsection}[1]{{\rmfamily\subsubsection{#1}}}
|
|
39 |
% isabelle in-text command font
|
|
40 |
\newcommand{\isacom}[1]{\isa{\isacommand{#1}}}
|
|
41 |
|
|
42 |
\protected\def\isacharunderscore{\raisebox{2pt}{\_\kern-1.7pt}}
|
|
43 |
\protected\def\isacharunderscorekeyword{\raisebox{2pt}{\_}}
|
|
44 |
% isabelle keyword, adapted from isabelle.sty
|
|
45 |
\renewcommand{\isakeyword}[1]
|
|
46 |
{\emph{\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
|
|
47 |
\def\isacharbraceleft{\{}\def\isacharbraceright{\}}\textsf{\textbf{#1}}}}
|
|
48 |
|
|
49 |
% add \noindent to text blocks automatically
|
|
50 |
\renewenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}}
|
|
51 |
\renewenvironment{isamarkuptxt}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}}
|
|
52 |
|
|
53 |
\newcommand{\noquotes}[1]{{\renewcommand{\isachardoublequote}{}\renewcommand{\isachardoublequoteopen}{}\renewcommand{\isachardoublequoteclose}{}#1}}
|
|
54 |
\newcommand{\xsymbol}[1]{\texttt{\char`\\\char`<#1>}}
|
|
55 |
|
|
56 |
%index
|
|
57 |
\newcommand{\conceptnoidx}[1]{\textbf{#1}}
|
|
58 |
\newcommand{\concept}[1]{\conceptnoidx{#1}\index{#1}}
|
|
59 |
\newcommand{\conceptidx}[2]{\conceptnoidx{#1}\index{#2}}
|
|
60 |
\newcommand{\indexed}[2]{#1\index{#2@\protect#1}}
|
|
61 |
|
|
62 |
\chardef\isachardoublequote=`\"%
|
|
63 |
\chardef\isachardoublequoteopen=`\"%
|
|
64 |
\chardef\isachardoublequoteclose=`\"%
|
|
65 |
|
|
66 |
\renewcommand{\isacharbackquoteopen}{\isacharbackquote}
|
|
67 |
\renewcommand{\isacharbackquoteclose}{\isacharbackquote}
|
|
68 |
|
|
69 |
\hyphenation{Isa-belle}
|