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