src/Doc/Prog_Prove/document/prelude.tex
author wenzelm
Sun, 02 Nov 2014 17:39:52 +0100
changeset 58885 47fdd4f40d00
parent 56451 856492b0f755
child 73511 2cdbb6a2f2a7
permissions -rw-r--r--
obsolete;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     1
\usepackage{makeidx}         % allows index generation
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     2
\usepackage{graphicx}        % standard LaTeX graphics tool
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     3
                             % when including figure files
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     4
\usepackage{multicol}        % used for the two-column index
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     5
\usepackage[bottom]{footmisc}% places footnotes at page bottom
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     6
\usepackage{alltt}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     7
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     8
\usepackage[T1]{fontenc}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     9
\usepackage{ccfonts}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    10
\usepackage[euler-digits]{eulervm}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    11
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    12
\usepackage{isabelle,isabellesym}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    13
\usepackage{mathpartir}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    14
\usepackage{amssymb}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    15
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    16
\renewcommand*\descriptionlabel[1]{\hspace\labelsep \textbf{#1}\hfil}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    17
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    18
% this should be the last package used
51463
fa84494bf3a0 get rid of xcolor warnings
nipkow
parents: 51448
diff changeset
    19
\usepackage{xcolor}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    20
\definecolor{linkcolor}{rgb}{0,0,0.4}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    21
\usepackage[colorlinks=true,linkcolor=linkcolor,citecolor=linkcolor,
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    22
            filecolor=linkcolor,pagecolor=linkcolor,
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    23
            urlcolor=linkcolor]{hyperref}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    24
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    25
% urls in roman style, theory text in math-similar italics
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    26
\urlstyle{tt}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    27
\isabellestyle{it}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    28
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    29
\renewcommand{\isadigit}[1]{\ensuremath{#1}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    30
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    31
% font size
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    32
\renewcommand{\isastyle}{\isastyleminor}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    33
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    34
% indexing
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    35
\usepackage{ifthen}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    36
\newcommand{\indexdef}[3]%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    37
{\ifthenelse{\equal{}{#1}}{\index{#3 (#2)|bold}}{\index{#3 (#1\ #2)|bold}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    38
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    39
% section commands
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    40
\renewcommand{\chapterautorefname}{Chapter}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    41
\renewcommand{\sectionautorefname}{Section}
51448
nipkow
parents: 51436
diff changeset
    42
\renewcommand{\subsectionautorefname}{Section}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    43
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    44
\renewcommand{\isamarkupsection}[1]{{\rmfamily\subsection{#1}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    45
\renewcommand{\isamarkupsubsection}[1]{{\rmfamily\subsubsection{#1}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    46
% isabelle in-text command font
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    47
\newcommand{\isacom}[1]{\isa{\isacommand{#1}}}
49627
34ada66545ca tuned printing of _ in latex
nipkow
parents: 49615
diff changeset
    48
34ada66545ca tuned printing of _ in latex
nipkow
parents: 49615
diff changeset
    49
\protected\def\isacharunderscore{\raisebox{2pt}{\_\kern-1.7pt}}
34ada66545ca tuned printing of _ in latex
nipkow
parents: 49615
diff changeset
    50
\protected\def\isacharunderscorekeyword{\raisebox{2pt}{\_}}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    51
% isabelle keyword, adapted from isabelle.sty
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    52
\renewcommand{\isakeyword}[1]
49627
34ada66545ca tuned printing of _ in latex
nipkow
parents: 49615
diff changeset
    53
{\emph{\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
51436
790310525e97 tuned (in particular bold fonts)
nipkow
parents: 49627
diff changeset
    54
\def\isacharbraceleft{\{}\def\isacharbraceright{\}}\def\bfdefault{sbc}\textbf{#1}}}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    55
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    56
% add \noindent to text blocks automatically
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    57
\renewenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    58
\renewenvironment{isamarkuptxt}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    59
49615
nipkow
parents: 48985
diff changeset
    60
\newcommand{\noquotes}[1]{{\renewcommand{\isachardoublequote}{}\renewcommand{\isachardoublequoteopen}{}\renewcommand{\isachardoublequoteclose}{}#1}}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    61
\newcommand{\xsymbol}[1]{\texttt{\char`\\\char`<#1>}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    62
55317
834a84553e02 started index
nipkow
parents: 51532
diff changeset
    63
%index
834a84553e02 started index
nipkow
parents: 51532
diff changeset
    64
\newcommand{\conceptnoidx}[1]{\textbf{#1}}
834a84553e02 started index
nipkow
parents: 51532
diff changeset
    65
\newcommand{\concept}[1]{\conceptnoidx{#1}\index{#1}}
834a84553e02 started index
nipkow
parents: 51532
diff changeset
    66
\newcommand{\conceptidx}[2]{\conceptnoidx{#1}\index{#2}}
55319
e33f25233798 tuned latex
nipkow
parents: 55317
diff changeset
    67
\newcommand{\indexed}[2]{#1\index{#2@\protect#1}}
55317
834a84553e02 started index
nipkow
parents: 51532
diff changeset
    68
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    69
\newcommand{\isabox}{\fbox}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    70
\newcommand{\bigisabox}[1]
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    71
{\isabox{\renewcommand{\isanewline}{\\}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    72
 \begin{tabular}{l}#1\end{tabular}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    73
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    74
%%%% ``WARNING'' environment: 2 ! characters separated by negative thin space
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    75
%\def\warnbang{\vtop to 0pt{\vss\hbox{\let\bfdefault=\bfdefaultold\Huge\textbf{!$\!$!}}\vss}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    76
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    77
\def\warnbang{\vtop to 0pt{\vss\hbox{\includegraphics[width=3ex, height=5.5ex]{bang}}\vss}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    78
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    79
\newenvironment{warn}{\begin{trivlist}\small\item[]\noindent%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    80
    \begingroup\hangindent=\parindent\hangafter=-2%\clubpenalty=10000%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    81
    \def\par{\endgraf\endgroup}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    82
    \hbox to0pt{\hskip-\hangindent\warnbang\hfill}\ignorespaces}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    83
  {\par\end{trivlist}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    84
47302
70239da25ef6 towards showing " in the tutorial
nipkow
parents: 47269
diff changeset
    85
\chardef\isachardoublequote=`\"%
70239da25ef6 towards showing " in the tutorial
nipkow
parents: 47269
diff changeset
    86
\chardef\isachardoublequoteopen=`\"%
70239da25ef6 towards showing " in the tutorial
nipkow
parents: 47269
diff changeset
    87
\chardef\isachardoublequoteclose=`\"%
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    88
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    89
\renewcommand{\isacharbackquoteopen}{\isacharbackquote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    90
\renewcommand{\isacharbackquoteclose}{\isacharbackquote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    91
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    92
\hyphenation{Isa-belle}