1.1 --- a/doc-src/springer.tex	Thu Mar 24 18:00:11 1994 +0100
     1.2 +++ b/doc-src/springer.tex	Thu Mar 24 18:14:45 1994 +0100
     1.3 @@ -1,9 +1,10 @@
     1.4 +%% $ lcp Exp $
     1.5  \documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book}
     1.6 -%%%\includeonly{preface}
     1.7 +%%%\includeonly{Ref/tctical,Ref/thm}
     1.8  %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}
     1.9  %% run    sedindex springer    to prepare index file
    1.10  
    1.11 -\sloppy%%%????????????????????????????????????????????????????????????????
    1.12 +\sloppy
    1.13  
    1.14  \title{Isabelle\\A Generic Theorem Prover}
    1.15  \author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow}
    1.16 @@ -15,7 +16,7 @@
    1.17  
    1.18  \underscoreoff
    1.19  
    1.20 -\setcounter{secnumdepth}{1} \setcounter{tocdepth}{1}
    1.21 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{1}
    1.22  
    1.23  \binperiod     %%%treat . like a binary operator
    1.24  
    1.25 @@ -44,10 +45,11 @@
    1.26  \end{quote}
    1.27  
    1.28  
    1.29 +\index{type classes|see{classes}}
    1.30  \index{definitions|see{rewriting, meta-level}}
    1.31  \index{rewriting!object-level|see{simplification}}
    1.32  \index{rules!meta-level|see{meta-rules}}
    1.33 -\index{scheme variables|see{unknowns}}
    1.34 +\index{variables!schematic|see{unknowns}} 
    1.35  \index{AST|see{trees, abstract syntax}}
    1.36  
    1.37  \part{Introduction to Isabelle}