doc-src/Ref/ref.tex

A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.

\documentclass[12pt,a4paper]{report}
\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../rail,../pdfsetup}

%% $Id$
%%\includeonly{}
%%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}
%%% to delete old ones:  \\indexbold{\*[^}]*}
%% run    sedindex ref    to prepare index file
%%% needs chapter on Provers/typedsimp.ML?
\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle Reference Manual}

\author{{\em Lawrence C. Paulson}\\
        Computer Laboratory \\ University of Cambridge \\
        \texttt{[e-mail]}\\[3ex] 
        With Contributions by Tobias Nipkow and Markus Wenzel}  

\makeindex

\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}

\pagestyle{headings}
\sloppy
\binperiod     %%%treat . like a binary operator

\railalias{lbrace}{\ttlbrace}
\railalias{rbrace}{\ttrbrace}
\railterm{lbrace,rbrace}

\begin{document}
\underscoreoff

\index{definitions|see{rewriting, meta-level}}
\index{rewriting!object-level|see{simplification}}
\index{meta-rules|see{meta-rules}}

\maketitle 
\emph{Note}: this document is part of the earlier Isabelle documentation, 
which is somewhat superseded by the Isabelle/HOL
\emph{Tutorial}~\cite{isa-tutorial}. Much of it is concerned with 
the old-style theory syntax and the primitives for conducting proofs 
using the ML top level. This style of interaction is largely obsolete:
most Isabelle proofs are now written using the Isar 
language and the Proof General interface. However, this is the only
comprehensive Isabelle reference manual.  

See also the \emph{Introduction to Isabelle}, which has tutorial examples
on conducting proofs using the ML top-level.

\subsubsection*{Acknowledgements} 
Tobias Nipkow, of T. U. Munich, wrote most of
  Chapters~\protect\ref{Defining-Logics} and~\protect\ref{chap:simplification},
  and part of
  Chapter~\protect\ref{theories}.  Carsten Clasohm also contributed to
  Chapter~\protect\ref{theories}.  Markus Wenzel contributed to
  Chapter~\protect\ref{chap:syntax}.  Jeremy Dawson, Sara Kalvala, Martin
  Simons  and others suggested changes
  and corrections.  The research has been funded by the EPSRC (grants
  GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT
  (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG
  Schwerpunktprogramm \emph{Deduktion}.

\pagenumbering{roman} \tableofcontents \clearfirst

\include{introduction}
\include{goals}
\include{tactic}
\include{tctical}
\include{thm}
\include{theories}
\include{defining}
\include{syntax}
\include{substitution}
\include{simplifier}
\include{classical}

%%seealso's must be last so that they appear last in the index entries
\index{meta-rewriting|seealso{tactics, theorems}}

\begingroup
  \bibliographystyle{plain} \small\raggedright\frenchspacing
  \bibliography{../manual}
\endgroup
\include{theory-syntax}

\printindex
\end{document}