src/Doc/How_to_Prove_it/document/prelude.tex

Simplified some proofs

\usepackage{makeidx}         % allows index generation
\usepackage{graphicx}        % standard LaTeX graphics tool
                             % when including figure files
\usepackage{multicol}        % used for the two-column index
\usepackage[bottom]{footmisc}% places footnotes at page bottom

\usepackage[T1]{fontenc}

\usepackage{isabelle,isabellesym}
%\usepackage{amssymb}

\renewcommand*\descriptionlabel[1]{\hspace\labelsep \textbf{#1}\hfil}

% this should be the last package used
\usepackage{xcolor}
\definecolor{linkcolor}{rgb}{0,0,0.4}
\usepackage[colorlinks=true,linkcolor=linkcolor,citecolor=linkcolor,
            filecolor=linkcolor,pagecolor=linkcolor,
            urlcolor=linkcolor]{hyperref}

% urls in roman style, theory text in math-similar italics
\urlstyle{tt}
\isabellestyle{it}

\renewcommand{\isadigit}[1]{\ensuremath{#1}}

% font size
\renewcommand{\isastyle}{\isastyleminor}

% indexing
\usepackage{ifthen}
\newcommand{\indexdef}[3]%
{\ifthenelse{\equal{}{#1}}{\index{#3 (#2)|bold}}{\index{#3 (#1\ #2)|bold}}}

\renewcommand{\isamarkupsection}[1]{{\rmfamily\subsection{#1}}}
\renewcommand{\isamarkupsubsection}[1]{{\rmfamily\subsubsection{#1}}}
% isabelle in-text command font
\newcommand{\isacom}[1]{\isa{\isacommand{#1}}}

\protected\def\isacharunderscore{\raisebox{2pt}{\_\kern-1.7pt}}
\protected\def\isacharunderscorekeyword{\raisebox{2pt}{\_}}
% isabelle keyword, adapted from isabelle.sty
\renewcommand{\isakeyword}[1]
{\emph{\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
\def\isacharbraceleft{\{}\def\isacharbraceright{\}}\textsf{\textbf{#1}}}}

% add \noindent to text blocks automatically
\renewenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}}
\renewenvironment{isamarkuptxt}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}}

\newcommand{\noquotes}[1]{{\renewcommand{\isachardoublequote}{}\renewcommand{\isachardoublequoteopen}{}\renewcommand{\isachardoublequoteclose}{}#1}}
\newcommand{\xsymbol}[1]{\texttt{\char`\\\char`<#1>}}

%index
\newcommand{\conceptnoidx}[1]{\textbf{#1}}
\newcommand{\concept}[1]{\conceptnoidx{#1}\index{#1}}
\newcommand{\conceptidx}[2]{\conceptnoidx{#1}\index{#2}}
\newcommand{\indexed}[2]{#1\index{#2@\protect#1}}

\chardef\isachardoublequote=`\"%
\chardef\isachardoublequoteopen=`\"%
\chardef\isachardoublequoteclose=`\"%

\renewcommand{\isacharbackquoteopen}{\isacharbackquote}
\renewcommand{\isacharbackquoteclose}{\isacharbackquote}

\hyphenation{Isa-belle}