src/HOL/Tools/Presburger/cooper_dec.ML
Mon, 14 Jun 2004 16:46:48 +0200 chaieb Oracle corrected
Sat, 12 Jun 2004 13:50:55 +0200 chaieb An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
Sat, 05 Jun 2004 18:34:06 +0200 chaieb More readable code.
Wed, 19 May 2004 11:23:59 +0200 chaieb A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
Tue, 25 Mar 2003 09:47:05 +0100 berghofe New decision procedure for Presburger arithmetic.
less more (0) tip