1 %% $ lcp Exp $ |
1 %% $ lcp Exp $ |
2 \documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book} |
2 \documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book} |
3 %%\includeonly{Logics/HOL} |
3 %\includeonly{Ref/simplifier} |
4 %% index{\(\w+\)\!meta-level index{meta-\1 |
4 %% index{\(\w+\)\!meta-level index{meta-\1 |
5 %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\) [\\ttindexbold{\1} |
5 %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\) [\\ttindexbold{\1} |
6 %% run sedindex springer to prepare index file |
6 %% run sedindex springer to prepare index file |
7 |
7 |
8 \sloppy |
8 \sloppy |
10 \title{Isabelle\\A Generic Theorem Prover} |
10 \title{Isabelle\\A Generic Theorem Prover} |
11 \author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow} |
11 \author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow} |
12 |
12 |
13 \date{} |
13 \date{} |
14 \makeindex |
14 \makeindex |
15 \let\idx=\ttindexbold |
|
16 %for indexing constants, symbols, theorems, ... |
|
17 \newcommand\cdx[1]{{\tt#1}\index{#1@{\tt#1} constant}} |
|
18 \newcommand\sdx[1]{{\tt#1}\index{#1@{\tt#1} symbol}} |
|
19 |
|
20 \newcommand\tdx[1]{{\tt#1}\index{#1@{\tt#1} theorem}} |
|
21 \newcommand\tdxbold[1]{{\tt#1}\index{#1@{\tt#1} theorem|bold}} |
|
22 |
|
23 \newcommand\mltydx[1]{{\tt#1}\index{#1@{\tt#1} ML type}} |
|
24 \newcommand\xdx[1]{{\tt#1}\index{#1@{\tt#1} exception}} |
|
25 |
|
26 \newcommand\ndx[1]{{\tt#1}\index{#1@{\tt#1} nonterminal}} |
|
27 \newcommand\ndxbold[1]{{\tt#1}\index{#1@{\tt#1} nonterminal|bold}} |
|
28 |
|
29 \newcommand\cldx[1]{{\tt#1}\index{#1@{\tt#1} class}} |
|
30 \newcommand\tydx[1]{{\tt#1}\index{#1@{\tt#1} type}} |
|
31 \newcommand\thydx[1]{{\tt#1}\index{#1@{\tt#1} theory}} |
|
32 |
15 |
33 \def\S{Sect.\thinspace}%This is how Springer like it |
16 \def\S{Sect.\thinspace}%This is how Springer like it |
34 |
17 |
35 \underscoreoff |
18 \underscoreoff |
36 |
19 |
47 \tableofcontents |
30 \tableofcontents |
48 \newpage |
31 \newpage |
49 \listoffigures |
32 \listoffigures |
50 \newpage |
33 \newpage |
51 |
34 |
52 \pagenumbering{arabic} |
|
53 |
|
54 \markboth{}{} |
35 \markboth{}{} |
55 \newfont{\sanssi}{cmssi12} |
36 \newfont{\sanssi}{cmssi12} |
56 \vspace*{2.5cm} |
37 \vspace*{2.5cm} |
57 \begin{quote} |
38 \begin{quote}\raggedleft |
58 \raggedleft |
39 {\em To Nathan and Sarah} |
|
40 |
|
41 \vspace*{1.2cm} |
59 {\sanssi |
42 {\sanssi |
60 You can only find truth with logic\\ |
43 You can only find truth with logic\\ |
61 if you have already found truth without it.}\\ |
44 if you have already found truth without it.}\\ |
62 \bigskip |
45 \bigskip |
63 |
46 |
64 G.K. Chesterton, {\em The Man who was Orthodox} |
47 G.K. Chesterton, {\em The Man who was Orthodox} |
65 \end{quote} |
48 \end{quote} |
66 |
49 |
|
50 \thispagestyle{empty} |
|
51 \newpage |
|
52 \pagenumbering{arabic} |
|
53 \part{Introduction to Isabelle} |
67 |
54 |
68 \index{hypotheses|see{assumptions}} |
55 \index{hypotheses|see{assumptions}} |
69 \index{rewriting|see{simplification}} |
56 \index{rewriting|see{simplification}} |
70 \index{variables!schematic|see{unknowns}} |
57 \index{variables!schematic|see{unknowns}} |
71 \index{abstract syntax trees|see{ASTs}} |
58 \index{abstract syntax trees|see{ASTs}} |
72 |
59 |
73 \part{Introduction to Isabelle} |
60 \begingroup%things local to Intro -- especially, redefining \part!! |
74 |
|
75 \begingroup |
|
76 \newcommand\qeq{\stackrel{?}{\equiv}} %for disagreement pairs in unification |
61 \newcommand\qeq{\stackrel{?}{\equiv}} %for disagreement pairs in unification |
77 \newcommand{\nand}{\mathbin{\lnot\&}} |
62 \newcommand{\nand}{\mathbin{\lnot\&}} |
78 \newcommand{\xor}{\mathbin{\#}} |
63 \newcommand{\xor}{\mathbin{\#}} |
79 \let\part=\chapter |
64 \let\part=\chapter |
80 \include{Intro/foundations} |
65 \include{Intro/foundations} |