src/HOL/Tools/lin_arith.ML
Sun, 01 Mar 2009 23:36:12 +0100 wenzelm use long names for old-style fold combinators;
Mon, 09 Feb 2009 22:14:33 +0100 nipkow fix to [arith]
Mon, 09 Feb 2009 18:50:10 +0100 nipkow new attribute "arith" for facts supplied to arith.
Sun, 18 Jan 2009 13:53:15 +0100 nipkow bug fixes
Sat, 17 Jan 2009 12:38:05 +0100 nipkow bug fix
Thu, 01 Jan 2009 14:23:39 +0100 wenzelm avoid polymorphic equality;
Thu, 28 Aug 2008 22:08:11 +0200 haftmann no parameter prefix for class interpretation
Thu, 29 May 2008 23:46:37 +0200 wenzelm added warning_count for issued reconstruction failure messages;
Sun, 18 May 2008 15:04:22 +0200 wenzelm renamed type decompT to decomp;
Fri, 22 Feb 2008 12:01:52 +0100 haftmann moved refute_tac to linarith.ML
Wed, 20 Feb 2008 14:52:38 +0100 haftmann tuned structures in arith_data.ML
Mon, 11 Feb 2008 22:12:19 +0100 huffman fix spelling
Tue, 15 Jan 2008 16:19:23 +0100 haftmann joined theories IntDef, Numeral, IntArith to theory Int
Fri, 12 Oct 2007 22:01:56 +0200 webertj typo in comment fixed
Tue, 09 Oct 2007 00:20:13 +0200 wenzelm generic Syntax.pretty/string_of operations;
Sat, 18 Aug 2007 19:25:28 +0200 webertj fixed a bug in demult: -a in (-a * b) is no longer treated as atomic
Tue, 14 Aug 2007 23:22:51 +0200 wenzelm avoid low-level tsig;
Thu, 09 Aug 2007 15:52:47 +0200 haftmann localized of_nat
Wed, 01 Aug 2007 16:55:40 +0200 wenzelm simplified internal Config interface;
Tue, 31 Jul 2007 19:40:23 +0200 wenzelm HOL setup for linear arithmetic -- moved here from arith_data.ML;
less more (0) tip