src/Doc/How_to_Prove_it/document/prelude.tex
changeset 56820 7fbed439b8d3
child 58873 db866dc081f8
equal deleted inserted replaced
56819:ad1bbed53788 56820:7fbed439b8d3
       
     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}