src/HOL/arith_data.ML
Tue, 13 Dec 2005 16:25:10 +0100 chaieb simpset for computation in raw_arith_tac added just as comment, nothing changed!
Thu, 01 Dec 2005 22:04:27 +0100 wenzelm simprocs: static evaluation of simpset;
Tue, 25 Oct 2005 18:38:21 +0200 wenzelm EVERY;
Tue, 25 Oct 2005 18:18:49 +0200 wenzelm avoid legacy goals;
Fri, 21 Oct 2005 18:14:38 +0200 wenzelm OldGoals;
Fri, 21 Oct 2005 14:49:04 +0200 haftmann introduced functions from Pure/General/rat.ML
Mon, 17 Oct 2005 23:10:10 +0200 wenzelm change_claset/simpset;
Fri, 23 Sep 2005 22:21:51 +0200 wenzelm Provers/Arith/fast_lin_arith.ML: Simplifier.inherit_bounds;
Mon, 12 Sep 2005 18:20:32 +0200 haftmann introduced new-style AList operations
Mon, 01 Aug 2005 19:20:23 +0200 wenzelm tuned msg;
Thu, 14 Jul 2005 19:28:16 +0200 wenzelm HOL.Not;
Thu, 07 Jul 2005 12:39:17 +0200 nipkow linear arithmetic now takes "&" in assumptions apart.
Mon, 20 Jun 2005 22:13:58 +0200 wenzelm get_thm instead of obsolete Goals.get_thm;
Mon, 20 Jun 2005 15:54:22 +0200 paulson moving some generic inequalities from integer arith to nat arith
Fri, 17 Jun 2005 18:33:05 +0200 wenzelm accomodate change of TheoryDataFun;
Fri, 10 Jun 2005 17:59:12 +0200 nipkow IntInf change
Mon, 16 May 2005 10:29:15 +0200 paulson Use of IntInf.int instead of int in most numeric simprocs; avoids
Fri, 13 May 2005 19:55:09 +0200 nipkow -(n::nat) is now regarded as atomic
Wed, 04 May 2005 10:42:43 +0200 nipkow fixed lin.arith
Wed, 04 May 2005 08:36:10 +0200 nipkow Fixing a problem with lin.arith.
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Thu, 07 Oct 2004 15:42:30 +0200 paulson simplification tweaks for better arithmetic reasoning
Fri, 01 Oct 2004 11:53:31 +0200 paulson tweaking of arithmetic proofs
Fri, 10 Sep 2004 20:04:14 +0200 nipkow Added antisymmetry simproc
Fri, 10 Sep 2004 00:19:15 +0200 nipkow new forward deduction capability for simplifier
Tue, 07 Sep 2004 11:42:50 +0200 nipkow tuned "discrete" field
Mon, 06 Sep 2004 17:37:35 +0200 nipkow made mult_mono_thms generic.
Fri, 06 Aug 2004 17:07:04 +0200 nipkow Initial changes to extend arithmetic from individual types to type classes.
Tue, 11 May 2004 20:11:08 +0200 obua changes made due to new Ring_and_Field theory
Fri, 02 Apr 2004 17:40:32 +0200 nipkow exposed fast_arith_neq_limit
Fri, 02 Apr 2004 14:47:11 +0200 nipkow got rid of ignore_neq again.
Fri, 02 Apr 2004 12:25:48 +0200 nipkow ignore_neq also influences arith_tac now, not just fast_arith_tac
Fri, 02 Apr 2004 12:08:38 +0200 nipkow Added ignore_neq flag.
Wed, 28 Jan 2004 10:41:49 +0100 paulson converted Real/Lubs to Isar script. Converting arithmetic setup
Wed, 14 Jan 2004 04:41:16 +0100 nipkow fixed old bugs in "decomp" (conversion from term to lin.arith. format).
Sat, 27 Dec 2003 21:02:14 +0100 paulson re-organized numeric lemmas
Mon, 07 Apr 2003 06:31:18 +0200 nipkow added isolate_Suc to counteract deficiencies in one of Larry's simprocs.
Tue, 25 Mar 2003 09:48:38 +0100 berghofe Added hook for presburger arithmetic decision procedure.
Fri, 23 Aug 2002 07:41:05 +0200 nipkow Added div+mod cancelling simproc
Tue, 13 Aug 2002 21:57:15 +0200 nipkow Counter example generation mods.
Tue, 06 Aug 2002 11:22:05 +0200 wenzelm sane interface for simprocs;
Tue, 26 Feb 2002 13:37:48 +0100 paulson Fixed the natxx_cancel_numerals simprocs so that they pull out Sucs and
Mon, 25 Feb 2002 10:42:34 +0100 nipkow solved the problem that Larry's simproce cancle_numerals(?) returns
Wed, 12 Dec 2001 19:19:59 +0100 nipkow tuned conversion from terms to "polynomials" for arith_tac: takes care
Sat, 01 Dec 2001 18:52:32 +0100 wenzelm renamed class "term" to "type" (actually "HOL.type");
Wed, 28 Nov 2001 00:46:26 +0100 wenzelm theory data: removed obsolete finish method;
Thu, 08 Nov 2001 23:59:37 +0100 wenzelm theory data: finish method;
Sun, 14 Oct 2001 20:02:59 +0200 wenzelm improved atomize setup;
Sat, 06 Oct 2001 00:02:46 +0200 wenzelm * sane numerals (stage 2): plain "num" syntax (removed "#");
Fri, 05 Oct 2001 21:52:39 +0200 wenzelm sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
Mon, 06 Aug 2001 13:43:24 +0200 nipkow turned translation for 1::nat into def.
Thu, 31 May 2001 16:07:35 +0200 nipkow Allow Suc-numerals as coefficients in lin-arith formulae
Tue, 16 Jan 2001 00:28:50 +0100 wenzelm tuned atomize;
Wed, 03 Jan 2001 11:14:48 +0100 paulson removal of the nat_cancel_factor simproc
Thu, 21 Dec 2000 16:19:39 +0100 nipkow rational arithmetic
Mon, 18 Dec 2000 14:59:05 +0100 nipkow moved mk_bin from Numerals to HOLogic
Fri, 01 Dec 2000 19:53:29 +0100 nipkow Linear arithmetic now copes with mixed nat/int formulae.
Thu, 23 Nov 2000 21:33:14 +0100 wenzelm arith_tac: atomize;
Thu, 07 Sep 2000 20:51:07 +0200 wenzelm tuned msg;
less more (0) -60 tip