src/HOL/Arith.ML
Tue, 23 May 2000 18:06:22 +0200 paulson added type constraint ::nat because 0 is now overloaded
Fri, 12 May 2000 14:59:12 +0200 paulson deleted some redundant simprules
Mon, 08 May 2000 16:58:18 +0200 paulson moved le_square, proved le_cube
Tue, 18 Apr 2000 15:56:41 +0200 paulson replaced obsolete diff_right_cancel by diff_diff_eq
Thu, 13 Apr 2000 15:18:02 +0200 paulson added some new iff-lemmas; removed some obsolete thms
Fri, 24 Mar 2000 20:59:15 +0100 wenzelm arith method: HEADGOAL;
Fri, 17 Mar 2000 17:11:59 +0100 wenzelm arith method: bang arg;
Mon, 13 Mar 2000 16:23:34 +0100 wenzelm case_tac now subsumes both boolean and datatype cases;
Mon, 13 Mar 2000 12:51:10 +0100 nipkow exhaust_tac -> cases_tac
Wed, 08 Mar 2000 16:13:19 +0100 paulson new lemmas
Fri, 18 Feb 2000 15:28:32 +0100 paulson new theorem nat_diff_split'
Wed, 05 Jan 2000 11:56:04 +0100 wenzelm replaced HOLogic.termTVar by HOLogic.termT;
Wed, 27 Oct 1999 12:50:48 +0200 paulson got rid of split_diff, which duplicated nat_diff_split, and
Tue, 28 Sep 1999 15:12:27 +0200 paulson zero_is_mult, by symmetry
Thu, 23 Sep 1999 09:04:36 +0200 nipkow Restructured lin.arith.package.
Tue, 21 Sep 1999 19:11:07 +0200 nipkow Mod because of new solver interface.
Tue, 21 Sep 1999 14:13:45 +0200 nipkow ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
Wed, 01 Sep 1999 21:25:55 +0200 wenzelm bind_thms;
Fri, 30 Jul 1999 13:42:57 +0200 wenzelm 'arith' proof method;
Fri, 30 Jul 1999 09:37:57 +0200 paulson split_diff and remove_diff_ss
Tue, 27 Jul 1999 22:04:30 +0200 wenzelm fixed comment;
Wed, 21 Jul 1999 15:26:17 +0200 paulson a stronger diff_less and no more le_diff_less
Thu, 15 Jul 1999 10:27:54 +0200 paulson qed_goal -> Goal
Tue, 13 Jul 1999 10:41:59 +0200 paulson simplified the <= monotonicity proof
Sat, 10 Jul 1999 21:48:27 +0200 wenzelm handle THM/TERM exn;
Thu, 01 Jul 1999 10:32:57 +0200 paulson new laws mult_le_cancel1, mult_le_cancel2
Wed, 17 Mar 1999 16:53:46 +0100 wenzelm Theory.sign_of;
Wed, 03 Mar 1999 11:15:18 +0100 paulson expandshort
Wed, 27 Jan 1999 17:11:39 +0100 nipkow arith_tac for min/max
Sun, 24 Jan 1999 11:33:54 +0100 nipkow Fixed a bug in lin.arith.
Thu, 14 Jan 1999 13:18:09 +0100 nipkow More arith refinements.
Wed, 13 Jan 1999 12:16:34 +0100 nipkow Refined arithmetic.
Wed, 13 Jan 1999 08:41:28 +0100 nipkow Simplified arithmetic.
Tue, 12 Jan 1999 15:59:35 +0100 nipkow Restructured Arithmatic
Mon, 11 Jan 1999 16:50:49 +0100 nipkow More arith simplifications.
Sat, 09 Jan 1999 17:55:54 +0100 nipkow Remoaved a few now redundant rewrite rules.
Sat, 09 Jan 1999 15:24:11 +0100 nipkow Refined arith tactic.
Tue, 05 Jan 1999 17:27:59 +0100 nipkow In Main: moved Bin to the left to preserve the solver in its simpset.
Mon, 04 Jan 1999 15:07:47 +0100 nipkow Version 1.0 of linear nat arithmetic.
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.
Fri, 23 Oct 1998 20:44:34 +0200 oheimb corrected auto_tac (applications of unsafe wrappers)
Fri, 16 Oct 1998 17:32:06 +0200 nipkow Installed trans_tac in solver of simpset().
Fri, 02 Oct 1998 10:41:35 +0200 paulson tidying
Thu, 01 Oct 1998 18:29:25 +0200 nipkow a few new lemmas.
Wed, 23 Sep 1998 10:12:01 +0200 paulson deleted needless parentheses
Fri, 18 Sep 1998 14:36:03 +0200 paulson theorem le_diff_conv2; tidying and expandshort
Mon, 14 Sep 1998 10:17:19 +0200 paulson new theorem le_diff_conv
Mon, 07 Sep 1998 10:40:17 +0200 paulson tidying
Fri, 04 Sep 1998 11:01:59 +0200 nipkow Arith: less_diff_conv
Tue, 01 Sep 1998 15:03:10 +0200 paulson changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
Tue, 01 Sep 1998 10:09:11 +0200 paulson Two new subtraction lemmas
Thu, 20 Aug 1998 16:58:28 +0200 paulson new theorems
Wed, 19 Aug 1998 10:26:02 +0200 paulson Some new theorems. zero_less_diff replaces less_imp_diff_positive
Tue, 18 Aug 1998 10:24:09 +0200 paulson new theorem diff_Suc_less_diff
Thu, 13 Aug 1998 18:14:26 +0200 paulson even more tidying of Goal commands
Thu, 06 Aug 1998 12:45:02 +0200 nipkow Removed duplicate thms:
Fri, 24 Jul 1998 13:03:20 +0200 berghofe Adapted to new datatype package.
Wed, 15 Jul 1998 10:15:13 +0200 paulson Removal of leading "\!\!..." from most Goal commands
Thu, 25 Jun 1998 13:57:34 +0200 paulson Installation of target HOL-Real
less more (0) -100 -60 tip