src/HOL/arith_data.ML
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