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.
%% $Id$
\documentclass[12pt,a4paper,fleqn]{report}
\usepackage{latexsym,graphicx,../iman,../extra,../ttbox,../proof,../rail,../railsetup,../isar,../pdfsetup}
\title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
\author{\emph{Markus Wenzel} \\ TU M\"unchen}
\makeindex
\newcommand{\isastyle}{\small\tt\slshape}
\newcommand{\isa}[1]{\emph{\isastyle #1}}
\newcommand{\isamath}[1]{\emph{$#1$}}
\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
\newcommand{\isasymequiv}{\isamath{\equiv}}
\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
\railterm{percent,ppercent,underscore,lbrace,rbrace,atsign}
\railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
\railterm{name,nameref,text,type,term,prop,atom}
\railalias{ident}{\railtok{ident}}
\railalias{longident}{\railtok{longident}}
\railalias{symident}{\railtok{symident}}
\railalias{var}{\railtok{var}}
\railalias{textvar}{\railtok{textvar}}
\railalias{typefree}{\railtok{typefree}}
\railalias{typevar}{\railtok{typevar}}
\railalias{nat}{\railtok{nat}}
\railalias{string}{\railtok{string}}
\railalias{verbatim}{\railtok{verbatim}}
\railalias{keyword}{\railtok{keyword}}
\railalias{name}{\railqtok{name}}
\railalias{nameref}{\railqtok{nameref}}
\railalias{text}{\railqtok{text}}
\railalias{type}{\railqtok{type}}
\railalias{term}{\railqtok{term}}
\railalias{prop}{\railqtok{prop}}
\railalias{atom}{\railqtok{atom}}
\newcommand{\drv}{\mathrel{\vdash}}
\newcommand{\edrv}{\mathop{\drv}\nolimits}
\newcommand{\Or}{\mathrel{\;|\;}}
\renewcommand{\vec}[1]{\overline{#1}}
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
\pagestyle{headings}
\sloppy
\binperiod %%%treat . like a binary operator
\renewcommand{\phi}{\varphi}
%\includeonly{}
\begin{document}
\underscoreoff
\maketitle
\pagenumbering{roman} \tableofcontents \clearfirst
\include{intro}
\include{basics}
\include{syntax}
\include{pure}
\include{generic}
\include{logics}
\appendix
\include{refcard}
\include{conversion}
\begingroup
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{../manual}
\endgroup
\printindex
\end{document}