src/HOL/Arith.ML
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
Mon, 22 Jun 1998 17:26:46 +0200 wenzelm isatool fixgoal;
Mon, 27 Apr 1998 16:45:11 +0200 nipkow Added a few lemmas.
Thu, 12 Mar 1998 10:37:58 +0100 paulson New laws, mostly generalizing old "pred" ones
Wed, 11 Mar 1998 11:03:43 +0100 paulson Arith.thy -> thy; proved a few new theorems
Sat, 07 Mar 1998 16:29:29 +0100 nipkow Removed `addsplits [expand_if]'
Tue, 03 Mar 1998 15:11:26 +0100 paulson New theorem diff_Suc_le_Suc_diff; tidied another proof
Tue, 16 Dec 1997 17:58:03 +0100 wenzelm expandshort;
Fri, 12 Dec 1997 10:31:25 +0100 paulson Faster proof of mult_less_cancel2
Sat, 06 Dec 1997 17:05:41 +0100 nipkow Got rid of some preds and replaced some n~=0 by 0<n.
Thu, 04 Dec 1997 12:44:37 +0100 nipkow pred n -> n-1
less more (0) -100 -60 tip