author | wenzelm |
Fri, 23 Mar 2018 17:09:36 +0100 | |
changeset 67933 | 604da273e18d |
parent 61409 | 9d68db31196c |
child 72319 | 76bb6dd505c0 |
permissions | -rw-r--r-- |
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 |
||
60185
cc71f01f9fde
prefer lmodern, which produces scalable T1 fonts even with Debian-ized TeXLive;
wenzelm
parents:
58873
diff
changeset
|
7 |
\usepackage{lmodern} |
56820 | 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} |