src/Doc/How_to_Prove_it/document/prelude.tex
author wenzelm
Sun Nov 02 16:50:42 2014 +0100 (2014-11-02)
changeset 58873 db866dc081f8
parent 56820 7fbed439b8d3
child 60185 cc71f01f9fde
permissions -rw-r--r--
obsolete;
     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{\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}