doc-src/springer.tex
changeset 358 df8f0fbf7dbd
parent 328 2d1b460dbb62
child 8828 5be2d1745c61
     1.1 --- a/doc-src/springer.tex	Tue May 03 18:27:30 1994 +0200
     1.2 +++ b/doc-src/springer.tex	Tue May 03 18:36:18 1994 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  %% $ lcp Exp $
     1.5  \documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book}
     1.6 -%%\includeonly{Logics/HOL}
     1.7 +%\includeonly{Ref/simplifier}
     1.8  %%  index{\(\w+\)\!meta-level     index{meta-\1
     1.9  %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}
    1.10  %% run    sedindex springer    to prepare index file
    1.11 @@ -12,23 +12,6 @@
    1.12  
    1.13  \date{} 
    1.14  \makeindex
    1.15 -\let\idx=\ttindexbold
    1.16 -%for indexing constants, symbols, theorems, ...
    1.17 -\newcommand\cdx[1]{{\tt#1}\index{#1@{\tt#1} constant}}
    1.18 -\newcommand\sdx[1]{{\tt#1}\index{#1@{\tt#1} symbol}}
    1.19 -
    1.20 -\newcommand\tdx[1]{{\tt#1}\index{#1@{\tt#1} theorem}}
    1.21 -\newcommand\tdxbold[1]{{\tt#1}\index{#1@{\tt#1} theorem|bold}}
    1.22 -
    1.23 -\newcommand\mltydx[1]{{\tt#1}\index{#1@{\tt#1} ML type}}
    1.24 -\newcommand\xdx[1]{{\tt#1}\index{#1@{\tt#1} exception}}
    1.25 -
    1.26 -\newcommand\ndx[1]{{\tt#1}\index{#1@{\tt#1} nonterminal}}
    1.27 -\newcommand\ndxbold[1]{{\tt#1}\index{#1@{\tt#1} nonterminal|bold}}
    1.28 -
    1.29 -\newcommand\cldx[1]{{\tt#1}\index{#1@{\tt#1} class}}
    1.30 -\newcommand\tydx[1]{{\tt#1}\index{#1@{\tt#1} type}}
    1.31 -\newcommand\thydx[1]{{\tt#1}\index{#1@{\tt#1} theory}}
    1.32  
    1.33  \def\S{Sect.\thinspace}%This is how Springer like it
    1.34  
    1.35 @@ -49,13 +32,13 @@
    1.36  \listoffigures
    1.37  \newpage
    1.38  
    1.39 -\pagenumbering{arabic}
    1.40 -
    1.41  \markboth{}{}
    1.42  \newfont{\sanssi}{cmssi12}
    1.43  \vspace*{2.5cm}
    1.44 -\begin{quote}
    1.45 -\raggedleft
    1.46 +\begin{quote}\raggedleft
    1.47 +{\em To Nathan and Sarah}
    1.48 +
    1.49 +\vspace*{1.2cm}
    1.50  {\sanssi
    1.51  You can only find truth with logic\\
    1.52  if you have already found truth without it.}\\
    1.53 @@ -64,15 +47,17 @@
    1.54  G.K. Chesterton, {\em The Man who was Orthodox}
    1.55  \end{quote}
    1.56  
    1.57 +\thispagestyle{empty}
    1.58 +\newpage
    1.59 +\pagenumbering{arabic}
    1.60 +\part{Introduction to Isabelle}   
    1.61  
    1.62  \index{hypotheses|see{assumptions}}
    1.63  \index{rewriting|see{simplification}}
    1.64  \index{variables!schematic|see{unknowns}} 
    1.65  \index{abstract syntax trees|see{ASTs}}
    1.66  
    1.67 -\part{Introduction to Isabelle}   
    1.68 -
    1.69 -\begingroup
    1.70 +\begingroup%things local to Intro -- especially, redefining \part!!
    1.71  \newcommand\qeq{\stackrel{?}{\equiv}}  %for disagreement pairs in unification
    1.72  \newcommand{\nand}{\mathbin{\lnot\&}} 
    1.73  \newcommand{\xor}{\mathbin{\#}}