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 7\usepackage{lmodern} 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{\isamarkupsection}[1]{{\rmfamily\subsection{#1}}} 37\renewcommand{\isamarkupsubsection}[1]{{\rmfamily\subsubsection{#1}}} 38% isabelle in-text command font 39\newcommand{\isacom}[1]{\isa{\isacommand{#1}}} 40 41\protected\def\isacharunderscore{\raisebox{2pt}{\_\kern-1.7pt}} 42\protected\def\isacharunderscorekeyword{\raisebox{2pt}{\_}} 43% isabelle keyword, adapted from isabelle.sty 44\renewcommand{\isakeyword}[1] 45{\emph{\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}% 46\def\isacharbraceleft{\{}\def\isacharbraceright{\}}\textsf{\textbf{#1}}}} 47 48% add \noindent to text blocks automatically 49\renewenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}} 50\renewenvironment{isamarkuptxt}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}} 51 52\newcommand{\noquotes}[1]{{\renewcommand{\isachardoublequote}{}\renewcommand{\isachardoublequoteopen}{}\renewcommand{\isachardoublequoteclose}{}#1}} 53\newcommand{\xsymbol}[1]{\texttt{\char`\\\char`<#1>}} 54 55%index 56\newcommand{\conceptnoidx}[1]{\textbf{#1}} 57\newcommand{\concept}[1]{\conceptnoidx{#1}\index{#1}} 58\newcommand{\conceptidx}[2]{\conceptnoidx{#1}\index{#2}} 59\newcommand{\indexed}[2]{#1\index{#2@\protect#1}} 60 61\chardef\isachardoublequote=`\"% 62\chardef\isachardoublequoteopen=`\"% 63\chardef\isachardoublequoteclose=`\"% 64 65\renewcommand{\isacharbackquoteopen}{\isacharbackquote} 66\renewcommand{\isacharbackquoteclose}{\isacharbackquote} 67 68\hyphenation{Isa-belle} 69