doc-src/springer.tex
changeset 328 2d1b460dbb62
parent 304 5edc4f5e5ebd
child 358 df8f0fbf7dbd
     1.1 --- a/doc-src/springer.tex	Fri Apr 15 18:10:49 1994 +0200
     1.2 +++ b/doc-src/springer.tex	Fri Apr 15 18:34:26 1994 +0200
     1.3 @@ -1,6 +1,7 @@
     1.4  %% $ lcp Exp $
     1.5  \documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book}
     1.6 -%%%\includeonly{Ref/tctical,Ref/thm}
     1.7 +%%\includeonly{Logics/HOL}
     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  
    1.12 @@ -12,6 +13,23 @@
    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  \underscoreoff
    1.36 @@ -28,6 +46,8 @@
    1.37  
    1.38  \tableofcontents
    1.39  \newpage
    1.40 +\listoffigures
    1.41 +\newpage
    1.42  
    1.43  \pagenumbering{arabic}
    1.44  
    1.45 @@ -45,12 +65,10 @@
    1.46  \end{quote}
    1.47  
    1.48  
    1.49 -\index{type classes|see{classes}}
    1.50 -\index{definitions|see{rewriting, meta-level}}
    1.51 -\index{rewriting!object-level|see{simplification}}
    1.52 -\index{rules!meta-level|see{meta-rules}}
    1.53 +\index{hypotheses|see{assumptions}}
    1.54 +\index{rewriting|see{simplification}}
    1.55  \index{variables!schematic|see{unknowns}} 
    1.56 -\index{AST|see{trees, abstract syntax}}
    1.57 +\index{abstract syntax trees|see{ASTs}}
    1.58  
    1.59  \part{Introduction to Isabelle}   
    1.60  
    1.61 @@ -71,6 +89,8 @@
    1.62  \include{Ref/tctical}
    1.63  \include{Ref/thm}
    1.64  \include{Ref/theories}
    1.65 +\include{Ref/defining}
    1.66 +\include{Ref/syntax}
    1.67  \include{Ref/substitution}
    1.68  \include{Ref/simplifier}
    1.69  \include{Ref/classical}
    1.70 @@ -78,18 +98,25 @@
    1.71  \part{Isabelle's Object-Logics} 
    1.72  \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
    1.73    \hrule\bigskip}
    1.74 +\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
    1.75 +
    1.76  \include{Logics/intro}
    1.77  \include{Logics/FOL}
    1.78  \include{Logics/ZF}
    1.79  \include{Logics/HOL}
    1.80  \include{Logics/LK}
    1.81  \include{Logics/CTT}
    1.82 -\include{Logics/defining}
    1.83  
    1.84  \include{Ref/theory-syntax}
    1.85  
    1.86  %%seealso's must be last so that they appear last in the index entries
    1.87 -\index{rewriting!meta-level|seealso{tactics, theorems}}
    1.88 +\index{backtracking|seealso{{\tt back} command, search}}
    1.89 +\index{classes|seealso{sorts}}
    1.90 +\index{sorts|seealso{arities}}
    1.91 +\index{axioms|seealso{rules, theorems}}
    1.92 +\index{theorems|seealso{rules}}
    1.93 +\index{definitions|seealso{meta-rewriting}}
    1.94 +\index{equality|seealso{simplification}}
    1.95  
    1.96  \bibliographystyle{springer} \small\raggedright\frenchspacing
    1.97  \bibliography{string-abbrv,atp,funprog,general,isabelle,logicprog,theory}