src/Doc/How_to_Prove_it/document/prelude.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/How_to_Prove_it/document/prelude.tex	Fri May 02 07:54:23 2014 +0200
@@ -0,0 +1,69 @@
+\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{alltt}
+
+\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{\isamarkupheader}[1]{{\rmfamily\subsection{#1}}}
+\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}