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.
<html>
<head><title>The Isabelle Library ({ISABELLE})</title></head>
<body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040">
<center>
<table width="100%" border="0" cellspacing="10" cellpadding="0">
<tr>
<td width="20%" valign="middle" align="center">
<img align=bottom src="isabelle.gif" width="100" height="86" alt="[Isabelle]">
</td>
<td width="80%" valign="middle" align="center">
<table width="90%" border="0" cellspacing="0" cellpadding="20">
<tr>
<td valign="middle" align="center" bgcolor="#aacccc">
<font face="Helvetica,Arial" size="+2">The Isabelle Library</font>
</td>
</tr>
</table>
</td>
</tr>
</table>
</center>
<hr>
Higher-Order Logic
<ul>
<li><a href="HOL/index.html">HOL (Higher-Order Logic)</a>
<li><a href="HOLCF/index.html">HOLCF (Higher-Order Logic of Computable Functions)</a>
</ul>
<hr>
First-Order Logic
<ul>
<li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a>
<li><a href="ZF/index.html">ZF (Set Theory)</a>
<li><a href="CCL/index.html">CCL (Classical Computational Logic)</a>
<li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a>
<li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a>
</ul>
<hr>
Miscellaneous
<ul>
<li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a>
<li><a href="CTT/index.html">CTT (Constructive Type Theory)</a>
<li><a href="Cube/index.html">Cube (The Lambda Cube)</a>
</ul>
<hr>
</body>
</html>