47269
|
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 |
|
47302
|
91 |
\chardef\isachardoublequote=`\"%
|
|
92 |
\chardef\isachardoublequoteopen=`\"%
|
|
93 |
\chardef\isachardoublequoteclose=`\"%
|
47269
|
94 |
|
|
95 |
\renewcommand{\isacharbackquoteopen}{\isacharbackquote}
|
|
96 |
\renewcommand{\isacharbackquoteclose}{\isacharbackquote}
|
|
97 |
|
|
98 |
\hyphenation{Isa-belle}
|