src/HOL/arith_data.ML
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;
Mon, 14 Aug 2000 14:57:29 +0200 wenzelm tuned names;
Tue, 25 Jul 2000 00:06:46 +0200 wenzelm rearranged setup of arithmetic procedures, avoiding global reference values;
Fri, 27 Nov 1998 17:00:30 +0100 nipkow At last: linear arithmetic for nat!
Wed, 28 Oct 1998 11:25:38 +0100 nipkow added nat_diff_split and a few lemmas in Trancl.
Thu, 01 Oct 1998 18:23:00 +0200 paulson tidied
Thu, 24 Sep 1998 17:17:14 +0200 oheimb renamed mk_meta_eq to mk_eq
Mon, 07 Sep 1998 10:40:17 +0200 paulson tidying
Tue, 01 Sep 1998 15:05:36 +0200 paulson Replaced Suc_diff_n by Suc_diff_le
Thu, 20 Aug 1998 16:44:05 +0200 paulson adjusted for new rewrites
Thu, 13 Aug 1998 18:14:26 +0200 paulson even more tidying of Goal commands
Wed, 12 Aug 1998 16:20:49 +0200 oheimb renamed mk_meta_eq to meta_eq
Sun, 12 Jul 1998 11:49:17 +0200 wenzelm isatool expandshort;
Tue, 03 Mar 1998 15:13:24 +0100 paulson New theorem
Fri, 05 Dec 1997 17:13:46 +0100 wenzelm simplification procedures nat_cancel enabled by default;
Mon, 01 Dec 1997 18:27:43 +0100 wenzelm open;
Mon, 01 Dec 1997 14:42:30 +0100 berghofe Added DiffCancelSums.
Thu, 27 Nov 1997 13:38:06 +0100 wenzelm mk_norm_sum;
Wed, 26 Nov 1997 17:52:53 +0100 wenzelm separate lists of simprocs;
Wed, 26 Nov 1997 16:44:25 +0100 wenzelm Setup various arithmetic proof procedures.
less more (0) tip