src/HOL/Tools/lin_arith.ML
Mon, 02 May 2011 16:33:21 +0200 wenzelm added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
Wed, 20 Apr 2011 22:57:29 +0200 wenzelm eliminated Display.string_of_thm_without_context;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Sat, 08 Jan 2011 00:28:31 +0100 wenzelm tuned;
Fri, 17 Dec 2010 13:45:43 +0100 wenzelm refer to regular structure Simplifier;
Sat, 28 Aug 2010 16:14:32 +0200 haftmann formerly unnamed infix equality now named HOL.eq
Fri, 27 Aug 2010 12:57:55 +0200 wenzelm merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
Fri, 27 Aug 2010 10:56:46 +0200 haftmann formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
Thu, 26 Aug 2010 20:42:09 +0200 wenzelm Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
Thu, 26 Aug 2010 17:37:26 +0200 wenzelm slightly more abstract data handling in Fast_Lin_Arith;
Wed, 25 Aug 2010 18:36:22 +0200 wenzelm renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
Thu, 19 Aug 2010 16:08:59 +0200 haftmann tuned quotes
Thu, 19 Aug 2010 11:02:14 +0200 haftmann use antiquotations for remaining unqualified constants in HOL
Mon, 19 Jul 2010 20:23:52 +0200 haftmann modernized abel_cancel simproc setup
Mon, 19 Jul 2010 16:09:43 +0200 haftmann discontinued pretending that abel_cancel is logic-independent; cleaned up junk
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
less more (0) -60 tip