wneuper/isa: doc-src/springer.tex@20e3616b2d9c

     1 %% $ lcp Exp $

     2 \documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book}

     3 %\includeonly{Ref/simplifier}

     4 %%  index{\(\w+\)\!meta-level     index{meta-\1

     5 %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}

     6 %% run    sedindex springer    to prepare index file

     8 \sloppy

    10 \title{Isabelle\\A Generic Theorem Prover}

    11 \author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow}

    13 \date{}

    14 \makeindex

    16 \def\S{Sect.\thinspace}%This is how Springer like it

    18 \underscoreoff

    20 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{1}

    22 \binperiod     %%%treat . like a binary operator

    24 \begin{document}

    25 \maketitle

    27 \pagenumbering{Roman}

    28 \include{preface}

    30 \tableofcontents

    31 \newpage

    32 \listoffigures

    33 \newpage

    35 \markboth{}{}

    36 \newfont{\sanssi}{cmssi12}

    37 \vspace*{2.5cm}

    38 \begin{quote}\raggedleft

    39 {\em To Nathan and Sarah}

    41 \vspace*{1.2cm}

    42 {\sanssi

    43 You can only find truth with logic\\

    44 if you have already found truth without it.}\\

    45 \bigskip

    47 G.K. Chesterton, {\em The Man who was Orthodox}

    48 \end{quote}

    50 \thispagestyle{empty}

    51 \newpage

    52 \pagenumbering{arabic}

    53 \part{Introduction to Isabelle}

    55 \index{hypotheses|see{assumptions}}

    56 \index{rewriting|see{simplification}}

    57 \index{variables!schematic|see{unknowns}}

    58 \index{abstract syntax trees|see{ASTs}}

    60 \begingroup%things local to Intro -- especially, redefining \part!!

    61 \newcommand\qeq{\stackrel{?}{\equiv}}  %for disagreement pairs in unification

    62 \newcommand{\nand}{\mathbin{\lnot\&}}

    63 \newcommand{\xor}{\mathbin{\#}}

    64 \let\part=\chapter

    65 \include{Intro/foundations}

    66 \include{Intro/getting}

    67 \include{Intro/advanced}

    68 \endgroup

    70 \part{The Isabelle Reference Manual}

    71 \include{Ref/introduction}

    72 \include{Ref/goals}

    73 \include{Ref/tactic}

    74 \include{Ref/tctical}

    75 \include{Ref/thm}

    76 \include{Ref/theories}

    77 \include{Ref/defining}

    78 \include{Ref/syntax}

    79 \include{Ref/substitution}

    80 \include{Ref/simplifier}

    81 \include{Ref/classical}

    83 \part{Isabelle's Object-Logics}

    84 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip

    85   \hrule\bigskip}

    86 \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}

    88 \include{Logics/intro}

    89 \include{Logics/FOL}

    90 \include{Logics/ZF}

    91 \include{Logics/HOL}

    92 \include{Logics/LK}

    93 \include{Logics/CTT}

    95 \include{Ref/theory-syntax}

    97 %%seealso's must be last so that they appear last in the index entries

    98 \index{backtracking|seealso{{\tt back} command, search}}

    99 \index{classes|seealso{sorts}}

   100 \index{sorts|seealso{arities}}

   101 \index{axioms|seealso{rules, theorems}}

   102 \index{theorems|seealso{rules}}

   103 \index{definitions|seealso{meta-rewriting}}

   104 \index{equality|seealso{simplification}}

   106 \bibliographystyle{springer} \small\raggedright\frenchspacing

   107 \bibliography{string-abbrv,atp,funprog,general,isabelle,logicprog,theory}

   109 \printindex

   110 \end{document}

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 12 Aug 2010 15:03:34 +0200
branch	isac-from-Isabelle2009-2
changeset 37913	20e3616b2d9c
parent 8828	5be2d1745c61
permissions	-rw-r--r--