src/HOL/Integ/presburger.ML
Fri, 21 May 2004 21:49:45 +0200 berghofe - deleted unneeded function eta_long (now in Pure/pattern.ML
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.
Mon, 12 Jan 2004 16:51:45 +0100 paulson Added lemmas to Ring_and_Field with slightly modified simplification rules
Thu, 24 Jul 2003 17:52:38 +0200 berghofe Fixed two bugs:
Sat, 10 May 2003 20:52:18 +0200 berghofe - Added split_min and split_max to preprocessor
Fri, 04 Apr 2003 17:01:12 +0200 berghofe Fixed bug in eta_long.
Tue, 25 Mar 2003 09:47:05 +0100 berghofe New decision procedure for Presburger arithmetic.
less more (0) tip