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