--- a/doc-src/springer.tex Tue Aug 28 13:12:03 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,110 +0,0 @@
-%% $ lcp Exp $
-\documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book}
-%\includeonly{Ref/simplifier}
-%% index{\(\w+\)\!meta-level index{meta-\1
-%%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\) [\\ttindexbold{\1}
-%% run sedindex springer to prepare index file
-
-\sloppy
-
-\title{Isabelle\\A Generic Theorem Prover}
-\author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow}
-
-\date{}
-\makeindex
-
-\def\S{Sect.\thinspace}%This is how Springer like it
-
-\underscoreoff
-
-\setcounter{secnumdepth}{2} \setcounter{tocdepth}{1}
-
-\binperiod %%%treat . like a binary operator
-
-\begin{document}
-\maketitle
-
-\pagenumbering{Roman}
-\include{preface}
-
-\tableofcontents
-\newpage
-\listoffigures
-\newpage
-
-\markboth{}{}
-\newfont{\sanssi}{cmssi12}
-\vspace*{2.5cm}
-\begin{quote}\raggedleft
-{\em To Nathan and Sarah}
-
-\vspace*{1.2cm}
-{\sanssi
-You can only find truth with logic\\
-if you have already found truth without it.}\\
-\bigskip
-
-G.K. Chesterton, {\em The Man who was Orthodox}
-\end{quote}
-
-\thispagestyle{empty}
-\newpage
-\pagenumbering{arabic}
-\part{Introduction to Isabelle}
-
-\index{hypotheses|see{assumptions}}
-\index{rewriting|see{simplification}}
-\index{variables!schematic|see{unknowns}}
-\index{abstract syntax trees|see{ASTs}}
-
-\begingroup%things local to Intro -- especially, redefining \part!!
-\newcommand\qeq{\stackrel{?}{\equiv}} %for disagreement pairs in unification
-\newcommand{\nand}{\mathbin{\lnot\&}}
-\newcommand{\xor}{\mathbin{\#}}
-\let\part=\chapter
-\include{Intro/foundations}
-\include{Intro/getting}
-\include{Intro/advanced}
-\endgroup
-
-\part{The Isabelle Reference Manual}
-\include{Ref/introduction}
-\include{Ref/goals}
-\include{Ref/tactic}
-\include{Ref/tctical}
-\include{Ref/thm}
-\include{Ref/theories}
-\include{Ref/defining}
-\include{Ref/syntax}
-\include{Ref/substitution}
-\include{Ref/simplifier}
-\include{Ref/classical}
-
-\part{Isabelle's Object-Logics}
-\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
- \hrule\bigskip}
-\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
-
-\include{Logics/intro}
-\include{Logics/FOL}
-\include{Logics/ZF}
-\include{Logics/HOL}
-\include{Logics/LK}
-\include{Logics/CTT}
-
-\include{Ref/theory-syntax}
-
-%%seealso's must be last so that they appear last in the index entries
-\index{backtracking|seealso{{\tt back} command, search}}
-\index{classes|seealso{sorts}}
-\index{sorts|seealso{arities}}
-\index{axioms|seealso{rules, theorems}}
-\index{theorems|seealso{rules}}
-\index{definitions|seealso{meta-rewriting}}
-\index{equality|seealso{simplification}}
-
-\bibliographystyle{springer} \small\raggedright\frenchspacing
-\bibliography{string-abbrv,atp,funprog,general,isabelle,logicprog,theory}
-
-\printindex
-\end{document}