equal
deleted
inserted
replaced
|
1 %% $ lcp Exp $ |
1 \documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book} |
2 \documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book} |
2 %%%\includeonly{preface} |
3 %%%\includeonly{Ref/tctical,Ref/thm} |
3 %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\) [\\ttindexbold{\1} |
4 %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\) [\\ttindexbold{\1} |
4 %% run sedindex springer to prepare index file |
5 %% run sedindex springer to prepare index file |
5 |
6 |
6 \sloppy%%%???????????????????????????????????????????????????????????????? |
7 \sloppy |
7 |
8 |
8 \title{Isabelle\\A Generic Theorem Prover} |
9 \title{Isabelle\\A Generic Theorem Prover} |
9 \author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow} |
10 \author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow} |
10 |
11 |
11 \date{} |
12 \date{} |
13 \let\idx=\ttindexbold |
14 \let\idx=\ttindexbold |
14 \def\S{Sect.\thinspace}%This is how Springer like it |
15 \def\S{Sect.\thinspace}%This is how Springer like it |
15 |
16 |
16 \underscoreoff |
17 \underscoreoff |
17 |
18 |
18 \setcounter{secnumdepth}{1} \setcounter{tocdepth}{1} |
19 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{1} |
19 |
20 |
20 \binperiod %%%treat . like a binary operator |
21 \binperiod %%%treat . like a binary operator |
21 |
22 |
22 \begin{document} |
23 \begin{document} |
23 \maketitle |
24 \maketitle |
42 |
43 |
43 G.K. Chesterton, {\em The Man who was Orthodox} |
44 G.K. Chesterton, {\em The Man who was Orthodox} |
44 \end{quote} |
45 \end{quote} |
45 |
46 |
46 |
47 |
|
48 \index{type classes|see{classes}} |
47 \index{definitions|see{rewriting, meta-level}} |
49 \index{definitions|see{rewriting, meta-level}} |
48 \index{rewriting!object-level|see{simplification}} |
50 \index{rewriting!object-level|see{simplification}} |
49 \index{rules!meta-level|see{meta-rules}} |
51 \index{rules!meta-level|see{meta-rules}} |
50 \index{scheme variables|see{unknowns}} |
52 \index{variables!schematic|see{unknowns}} |
51 \index{AST|see{trees, abstract syntax}} |
53 \index{AST|see{trees, abstract syntax}} |
52 |
54 |
53 \part{Introduction to Isabelle} |
55 \part{Introduction to Isabelle} |
54 |
56 |
55 \begingroup |
57 \begingroup |