src/HOL/arith_data.ML
Wed, 28 Nov 2007 09:01:40 +0100 haftmann dropped dead code
Tue, 31 Jul 2007 19:40:26 +0200 wenzelm moved lin_arith stuff to Tools/lin_arith.ML;
Tue, 31 Jul 2007 00:56:29 +0200 wenzelm arith method setup: proper context;
Fri, 20 Jul 2007 14:28:25 +0200 haftmann moved class ord from Orderings.thy to HOL.thy
Tue, 03 Jul 2007 17:17:04 +0200 wenzelm CONVERSION tactical;
Wed, 13 Jun 2007 03:31:11 +0200 huffman removed constant int :: nat => int;
Sat, 02 Jun 2007 08:54:05 +0200 webertj cosmetic
Fri, 01 Jun 2007 16:04:13 +0200 webertj fixed handling of meta-logic propositions
Thu, 24 May 2007 07:27:44 +0200 nipkow Introduced new classes monoid_add and group_add
Thu, 17 May 2007 19:49:40 +0200 haftmann canonical prefixing of class constants
Sun, 13 May 2007 18:15:22 +0200 haftmann refined module rat
Thu, 10 May 2007 22:11:35 +0200 haftmann fixed typo
Thu, 10 May 2007 00:39:45 +0200 wenzelm moved conversions to structure Conv;
Wed, 09 May 2007 07:53:08 +0200 haftmann tuned
Mon, 07 May 2007 00:49:59 +0200 wenzelm simplified DataFun interfaces;
Sun, 06 May 2007 21:49:23 +0200 haftmann tuned
Wed, 11 Apr 2007 08:28:15 +0200 haftmann canonical merge operations
Thu, 29 Mar 2007 14:21:45 +0200 haftmann dropped legacy ML bindings
Mon, 18 Dec 2006 08:21:35 +0100 haftmann switched argument order in *.syntax lifters
Wed, 13 Dec 2006 15:45:31 +0100 haftmann introduced mk/dest_numeral/number for mk/dest_binum etc.
Fri, 01 Dec 2006 17:22:31 +0100 haftmann slight cleanup in hologic.ML
Sat, 18 Nov 2006 00:20:22 +0100 haftmann op div/op mod now named without leading op
Wed, 08 Nov 2006 13:48:29 +0100 wenzelm removed theory NatArith (now part of Nat);
Mon, 09 Oct 2006 02:19:49 +0200 wenzelm attribute: Context.mapping;
Wed, 04 Oct 2006 18:41:14 +0200 nipkow fixed bug in linear arith
Wed, 04 Oct 2006 01:43:57 +0200 webertj nnf_simpset built statically
Tue, 26 Sep 2006 13:34:16 +0200 haftmann renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
Wed, 06 Sep 2006 13:48:02 +0200 haftmann got rid of Numeral.bin type
Fri, 25 Aug 2006 00:10:10 +0200 webertj avoid duplicate tactics
Thu, 24 Aug 2006 23:51:46 +0200 webertj additional list of tactics that can be added to arith
Wed, 02 Aug 2006 03:33:28 +0200 webertj type annotations fixed (IntInf.int, to make SML/NJ happy)
Tue, 01 Aug 2006 14:58:43 +0200 webertj possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
Mon, 31 Jul 2006 20:56:49 +0200 webertj fixed a bug in function poly: decomposition of products
Mon, 31 Jul 2006 15:29:36 +0200 webertj code reformatted
Sat, 29 Jul 2006 13:15:12 +0200 webertj lin_arith_prover splits certain operators (e.g. min, max, abs)
Wed, 26 Jul 2006 19:23:04 +0200 webertj linear arithmetic splits certain operators (e.g. min, max, abs)
Sat, 08 Jul 2006 12:54:30 +0200 wenzelm simprocs: no theory argument -- use simpset context instead;
Thu, 08 Jun 2006 13:49:39 +0200 nipkow replaced REPEAT by REPOEAT_DETERM
Thu, 27 Apr 2006 12:11:56 +0200 paulson renamed HOLogic.mk_bin to mk_binum for consistency with dest_binum
Tue, 21 Mar 2006 12:16:43 +0100 paulson Removal of unnecessary simprules: simproc cancel_numerals now works without
Fri, 17 Mar 2006 22:33:06 +0100 nipkow fixed problem with proof reconstruction by adding add_Suc to arith-simpset.
Fri, 17 Mar 2006 09:34:23 +0100 haftmann renamed op < <= to Orderings.less(_eq)
Fri, 10 Mar 2006 15:33:48 +0100 haftmann renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
Wed, 15 Feb 2006 18:10:09 +0100 webertj typo in a comment fixed
Sat, 21 Jan 2006 23:02:14 +0100 wenzelm simplified type attribute;
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
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
less more (0) -100 -60 tip