src/HOL/Tools/lin_arith.ML
Tue, 08 Jun 2010 16:37:22 +0200 haftmann tuned quotes, antiquotations and whitespace
Wed, 05 May 2010 18:25:34 +0200 haftmann farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
Sun, 28 Mar 2010 16:59:06 +0200 wenzelm static defaults for configuration options;
Mon, 22 Mar 2010 11:45:09 +0100 boehmes removed warning_count (known causes for warnings have been resolved)
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Sun, 28 Feb 2010 23:51:31 +0100 wenzelm more antiquotations;
Mon, 22 Feb 2010 09:17:49 +0100 haftmann merged
Fri, 19 Feb 2010 14:47:01 +0100 haftmann moved remaning class operations from Algebras.thy to Groups.thy
Fri, 19 Feb 2010 16:11:45 +0100 wenzelm renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
Fri, 19 Feb 2010 11:49:44 +0100 wenzelm Lin_Arith.pre_tac: inherit proper simplifier context, and get rid of posthoc renaming of bound variables;
Wed, 10 Feb 2010 14:12:04 +0100 haftmann moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
Wed, 10 Feb 2010 08:49:26 +0100 haftmann moved constants inverse and divide to Ring.thy
Mon, 08 Feb 2010 17:12:38 +0100 haftmann renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Thu, 28 Jan 2010 11:48:49 +0100 haftmann new theory Algebras.thy for generic algebraic structures
Tue, 17 Nov 2009 10:17:53 +0000 webertj Fixed splitting of div and mod on integers (split theorem differed from implementation).
Mon, 16 Nov 2009 18:33:12 +0000 webertj Fixed a typo in a comment.
Tue, 10 Nov 2009 18:11:23 +0100 wenzelm eliminated some unused/obsolete Args.bang_facts;
Sun, 08 Nov 2009 18:42:57 +0100 wenzelm tuned;
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Thu, 29 Oct 2009 23:56:33 +0100 wenzelm eliminated some old folds;
Thu, 29 Oct 2009 17:58:26 +0100 wenzelm standardized filter/filter_out;
Wed, 21 Oct 2009 00:36:12 +0200 wenzelm standardized basic operations on type option;
Fri, 02 Oct 2009 23:15:36 +0200 wenzelm eliminated dead code;
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Fri, 18 Sep 2009 09:07:50 +0200 haftmann tuned const_name antiquotations
Fri, 14 Aug 2009 13:44:14 +0100 webertj Fixed a bug where the simplifier would hang on
Tue, 21 Jul 2009 01:03:18 +0200 wenzelm proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
Mon, 08 Jun 2009 22:29:37 +0200 boehmes fast_lin_arith uses proper multiplication instead of unfolding to additions
Mon, 11 May 2009 15:57:29 +0200 haftmann qualified names for Lin_Arith tactics and simprocs
Mon, 11 May 2009 15:18:32 +0200 haftmann tuned interface of Lin_Arith
Sat, 09 May 2009 09:17:29 +0200 haftmann interface changes in linarith.ML
Thu, 26 Mar 2009 14:14:02 +0100 wenzelm simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
Mon, 23 Mar 2009 19:01:16 +0100 haftmann moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
Sun, 15 Mar 2009 15:59:44 +0100 wenzelm simplified attribute setup;
Fri, 13 Mar 2009 23:50:05 +0100 wenzelm simplified method setup;
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
Thu, 12 Mar 2009 18:01:26 +0100 haftmann vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
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