doc-src/springer.tex

clarified split_thy_path;

+
−%% $ 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}