doc-src/springer.tex
author haftmann
Tue Oct 10 13:59:12 2006 +0200 (2006-10-10)
changeset 20950 981fa0ce23ed
parent 8828 5be2d1745c61
permissions -rw-r--r--
added IsarAdvanced material
lcp@304
     1
%% $ lcp Exp $
lcp@285
     2
\documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book}
lcp@358
     3
%\includeonly{Ref/simplifier}
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@328
    15
lcp@285
    16
\def\S{Sect.\thinspace}%This is how Springer like it
lcp@285
    17
lcp@285
    18
\underscoreoff
lcp@285
    19
lcp@304
    20
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{1}
lcp@285
    21
lcp@285
    22
\binperiod     %%%treat . like a binary operator
lcp@285
    23
lcp@285
    24
\begin{document}
lcp@285
    25
\maketitle
lcp@285
    26
lcp@285
    27
\pagenumbering{Roman}
lcp@285
    28
\include{preface}
lcp@285
    29
lcp@285
    30
\tableofcontents
lcp@285
    31
\newpage
lcp@328
    32
\listoffigures
lcp@328
    33
\newpage
lcp@285
    34
lcp@285
    35
\markboth{}{}
lcp@285
    36
\newfont{\sanssi}{cmssi12}
lcp@285
    37
\vspace*{2.5cm}
lcp@358
    38
\begin{quote}\raggedleft
lcp@358
    39
{\em To Nathan and Sarah}
lcp@358
    40
lcp@358
    41
\vspace*{1.2cm}
lcp@285
    42
{\sanssi
lcp@285
    43
You can only find truth with logic\\
lcp@285
    44
if you have already found truth without it.}\\
lcp@285
    45
\bigskip
lcp@285
    46
lcp@285
    47
G.K. Chesterton, {\em The Man who was Orthodox}
lcp@285
    48
\end{quote}
lcp@285
    49
lcp@358
    50
\thispagestyle{empty}
lcp@358
    51
\newpage
lcp@358
    52
\pagenumbering{arabic}
lcp@358
    53
\part{Introduction to Isabelle}   
lcp@285
    54
lcp@328
    55
\index{hypotheses|see{assumptions}}
lcp@328
    56
\index{rewriting|see{simplification}}
lcp@304
    57
\index{variables!schematic|see{unknowns}} 
lcp@328
    58
\index{abstract syntax trees|see{ASTs}}
lcp@285
    59
lcp@358
    60
\begingroup%things local to Intro -- especially, redefining \part!!
lcp@285
    61
\newcommand\qeq{\stackrel{?}{\equiv}}  %for disagreement pairs in unification
lcp@285
    62
\newcommand{\nand}{\mathbin{\lnot\&}} 
lcp@285
    63
\newcommand{\xor}{\mathbin{\#}}
lcp@285
    64
\let\part=\chapter
lcp@285
    65
\include{Intro/foundations}
lcp@285
    66
\include{Intro/getting}
lcp@285
    67
\include{Intro/advanced}
lcp@285
    68
\endgroup
lcp@285
    69
lcp@285
    70
\part{The Isabelle Reference Manual} 
lcp@285
    71
\include{Ref/introduction}
lcp@285
    72
\include{Ref/goals}
lcp@285
    73
\include{Ref/tactic}
lcp@285
    74
\include{Ref/tctical}
lcp@285
    75
\include{Ref/thm}
lcp@285
    76
\include{Ref/theories}
lcp@328
    77
\include{Ref/defining}
lcp@328
    78
\include{Ref/syntax}
lcp@285
    79
\include{Ref/substitution}
lcp@285
    80
\include{Ref/simplifier}
lcp@285
    81
\include{Ref/classical}
lcp@285
    82
lcp@285
    83
\part{Isabelle's Object-Logics} 
lcp@285
    84
\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
lcp@285
    85
  \hrule\bigskip}
lcp@328
    86
\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
lcp@328
    87
lcp@285
    88
\include{Logics/intro}
lcp@285
    89
\include{Logics/FOL}
lcp@285
    90
\include{Logics/ZF}
lcp@285
    91
\include{Logics/HOL}
lcp@285
    92
\include{Logics/LK}
lcp@285
    93
\include{Logics/CTT}
lcp@285
    94
lcp@285
    95
\include{Ref/theory-syntax}
lcp@285
    96
lcp@285
    97
%%seealso's must be last so that they appear last in the index entries
lcp@328
    98
\index{backtracking|seealso{{\tt back} command, search}}
lcp@328
    99
\index{classes|seealso{sorts}}
lcp@328
   100
\index{sorts|seealso{arities}}
lcp@328
   101
\index{axioms|seealso{rules, theorems}}
lcp@328
   102
\index{theorems|seealso{rules}}
lcp@328
   103
\index{definitions|seealso{meta-rewriting}}
lcp@328
   104
\index{equality|seealso{simplification}}
lcp@285
   105
lcp@285
   106
\bibliographystyle{springer} \small\raggedright\frenchspacing
lcp@285
   107
\bibliography{string-abbrv,atp,funprog,general,isabelle,logicprog,theory}
lcp@285
   108
wenzelm@8828
   109
\printindex
lcp@285
   110
\end{document}