doc-src/springer.tex
author lcp
Mon Mar 21 10:51:28 1994 +0100 (1994-03-21)
changeset 285 fd4a6585e5bf
child 304 5edc4f5e5ebd
permissions -rw-r--r--
first draft of Springer book
lcp@285
     1
\documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book}
lcp@285
     2
%%%\includeonly{preface}
lcp@285
     3
%%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}
lcp@285
     4
%% run    sedindex springer    to prepare index file
lcp@285
     5
lcp@285
     6
\sloppy%%%????????????????????????????????????????????????????????????????
lcp@285
     7
lcp@285
     8
\title{Isabelle\\A Generic Theorem Prover}
lcp@285
     9
\author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow}
lcp@285
    10
lcp@285
    11
\date{} 
lcp@285
    12
\makeindex
lcp@285
    13
\let\idx=\ttindexbold
lcp@285
    14
\def\S{Sect.\thinspace}%This is how Springer like it
lcp@285
    15
lcp@285
    16
\underscoreoff
lcp@285
    17
lcp@285
    18
\setcounter{secnumdepth}{1} \setcounter{tocdepth}{1}
lcp@285
    19
lcp@285
    20
\binperiod     %%%treat . like a binary operator
lcp@285
    21
lcp@285
    22
\begin{document}
lcp@285
    23
\maketitle
lcp@285
    24
lcp@285
    25
\pagenumbering{Roman}
lcp@285
    26
\include{preface}
lcp@285
    27
lcp@285
    28
\tableofcontents
lcp@285
    29
\newpage
lcp@285
    30
lcp@285
    31
\pagenumbering{arabic}
lcp@285
    32
lcp@285
    33
\markboth{}{}
lcp@285
    34
\newfont{\sanssi}{cmssi12}
lcp@285
    35
\vspace*{2.5cm}
lcp@285
    36
\begin{quote}
lcp@285
    37
\raggedleft
lcp@285
    38
{\sanssi
lcp@285
    39
You can only find truth with logic\\
lcp@285
    40
if you have already found truth without it.}\\
lcp@285
    41
\bigskip
lcp@285
    42
lcp@285
    43
G.K. Chesterton, {\em The Man who was Orthodox}
lcp@285
    44
\end{quote}
lcp@285
    45
lcp@285
    46
lcp@285
    47
\index{definitions|see{rewriting, meta-level}}
lcp@285
    48
\index{rewriting!object-level|see{simplification}}
lcp@285
    49
\index{rules!meta-level|see{meta-rules}}
lcp@285
    50
\index{scheme variables|see{unknowns}}
lcp@285
    51
\index{AST|see{trees, abstract syntax}}
lcp@285
    52
lcp@285
    53
\part{Introduction to Isabelle}   
lcp@285
    54
lcp@285
    55
\begingroup
lcp@285
    56
\newcommand\qeq{\stackrel{?}{\equiv}}  %for disagreement pairs in unification
lcp@285
    57
\newcommand{\nand}{\mathbin{\lnot\&}} 
lcp@285
    58
\newcommand{\xor}{\mathbin{\#}}
lcp@285
    59
\let\part=\chapter
lcp@285
    60
\include{Intro/foundations}
lcp@285
    61
\include{Intro/getting}
lcp@285
    62
\include{Intro/advanced}
lcp@285
    63
\endgroup
lcp@285
    64
lcp@285
    65
\part{The Isabelle Reference Manual} 
lcp@285
    66
\include{Ref/introduction}
lcp@285
    67
\include{Ref/goals}
lcp@285
    68
\include{Ref/tactic}
lcp@285
    69
\include{Ref/tctical}
lcp@285
    70
\include{Ref/thm}
lcp@285
    71
\include{Ref/theories}
lcp@285
    72
\include{Ref/substitution}
lcp@285
    73
\include{Ref/simplifier}
lcp@285
    74
\include{Ref/classical}
lcp@285
    75
lcp@285
    76
\part{Isabelle's Object-Logics} 
lcp@285
    77
\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
lcp@285
    78
  \hrule\bigskip}
lcp@285
    79
\include{Logics/intro}
lcp@285
    80
\include{Logics/FOL}
lcp@285
    81
\include{Logics/ZF}
lcp@285
    82
\include{Logics/HOL}
lcp@285
    83
\include{Logics/LK}
lcp@285
    84
\include{Logics/CTT}
lcp@285
    85
\include{Logics/defining}
lcp@285
    86
lcp@285
    87
\include{Ref/theory-syntax}
lcp@285
    88
lcp@285
    89
%%seealso's must be last so that they appear last in the index entries
lcp@285
    90
\index{rewriting!meta-level|seealso{tactics, theorems}}
lcp@285
    91
lcp@285
    92
\bibliographystyle{springer} \small\raggedright\frenchspacing
lcp@285
    93
\bibliography{string-abbrv,atp,funprog,general,isabelle,logicprog,theory}
lcp@285
    94
lcp@285
    95
\input{springer.ind}
lcp@285
    96
\end{document}