| Mon, 13 Mar 2000 16:23:34 +0100 | wenzelm | case_tac now subsumes both boolean and datatype cases; | file | diff | annotate |
| Mon, 13 Mar 2000 12:51:10 +0100 | nipkow | exhaust_tac -> cases_tac | file | diff | annotate |
| Wed, 08 Mar 2000 16:13:19 +0100 | paulson | new lemmas | file | diff | annotate |
| Fri, 18 Feb 2000 15:28:32 +0100 | paulson | new theorem nat_diff_split' | file | diff | annotate |
| Wed, 05 Jan 2000 11:56:04 +0100 | wenzelm | replaced HOLogic.termTVar by HOLogic.termT; | file | diff | annotate |
| Wed, 27 Oct 1999 12:50:48 +0200 | paulson | got rid of split_diff, which duplicated nat_diff_split, and | file | diff | annotate |
| Tue, 28 Sep 1999 15:12:27 +0200 | paulson | zero_is_mult, by symmetry | file | diff | annotate |
| Thu, 23 Sep 1999 09:04:36 +0200 | nipkow | Restructured lin.arith.package. | file | diff | annotate |
| Tue, 21 Sep 1999 19:11:07 +0200 | nipkow | Mod because of new solver interface. | file | diff | annotate |
| Tue, 21 Sep 1999 14:13:45 +0200 | nipkow | ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML | file | diff | annotate |
| Wed, 01 Sep 1999 21:25:55 +0200 | wenzelm | bind_thms; | file | diff | annotate |
| Fri, 30 Jul 1999 13:42:57 +0200 | wenzelm | 'arith' proof method; | file | diff | annotate |
| Fri, 30 Jul 1999 09:37:57 +0200 | paulson | split_diff and remove_diff_ss | file | diff | annotate |
| Tue, 27 Jul 1999 22:04:30 +0200 | wenzelm | fixed comment; | file | diff | annotate |
| Wed, 21 Jul 1999 15:26:17 +0200 | paulson | a stronger diff_less and no more le_diff_less | file | diff | annotate |
| Thu, 15 Jul 1999 10:27:54 +0200 | paulson | qed_goal -> Goal | file | diff | annotate |
| Tue, 13 Jul 1999 10:41:59 +0200 | paulson | simplified the <= monotonicity proof | file | diff | annotate |
| Sat, 10 Jul 1999 21:48:27 +0200 | wenzelm | handle THM/TERM exn; | file | diff | annotate |
| Thu, 01 Jul 1999 10:32:57 +0200 | paulson | new laws mult_le_cancel1, mult_le_cancel2 | file | diff | annotate |
| Wed, 17 Mar 1999 16:53:46 +0100 | wenzelm | Theory.sign_of; | file | diff | annotate |
| Wed, 03 Mar 1999 11:15:18 +0100 | paulson | expandshort | file | diff | annotate |
| Wed, 27 Jan 1999 17:11:39 +0100 | nipkow | arith_tac for min/max | file | diff | annotate |
| Sun, 24 Jan 1999 11:33:54 +0100 | nipkow | Fixed a bug in lin.arith. | file | diff | annotate |
| Thu, 14 Jan 1999 13:18:09 +0100 | nipkow | More arith refinements. | file | diff | annotate |
| Wed, 13 Jan 1999 12:16:34 +0100 | nipkow | Refined arithmetic. | file | diff | annotate |
| Wed, 13 Jan 1999 08:41:28 +0100 | nipkow | Simplified arithmetic. | file | diff | annotate |
| Tue, 12 Jan 1999 15:59:35 +0100 | nipkow | Restructured Arithmatic | file | diff | annotate |
| Mon, 11 Jan 1999 16:50:49 +0100 | nipkow | More arith simplifications. | file | diff | annotate |
| Sat, 09 Jan 1999 17:55:54 +0100 | nipkow | Remoaved a few now redundant rewrite rules. | file | diff | annotate |
| Sat, 09 Jan 1999 15:24:11 +0100 | nipkow | Refined arith tactic. | file | diff | annotate |
| Tue, 05 Jan 1999 17:27:59 +0100 | nipkow | In Main: moved Bin to the left to preserve the solver in its simpset. | file | diff | annotate |
| Mon, 04 Jan 1999 15:07:47 +0100 | nipkow | Version 1.0 of linear nat arithmetic. | file | diff | annotate |
| Fri, 27 Nov 1998 17:00:30 +0100 | nipkow | At last: linear arithmetic for nat! | file | diff | annotate |
| Wed, 28 Oct 1998 11:25:38 +0100 | nipkow | added nat_diff_split and a few lemmas in Trancl. | file | diff | annotate |
| Fri, 23 Oct 1998 20:44:34 +0200 | oheimb | corrected auto_tac (applications of unsafe wrappers) | file | diff | annotate |
| Fri, 16 Oct 1998 17:32:06 +0200 | nipkow | Installed trans_tac in solver of simpset(). | file | diff | annotate |
| Fri, 02 Oct 1998 10:41:35 +0200 | paulson | tidying | file | diff | annotate |
| Thu, 01 Oct 1998 18:29:25 +0200 | nipkow | a few new lemmas. | file | diff | annotate |
| Wed, 23 Sep 1998 10:12:01 +0200 | paulson | deleted needless parentheses | file | diff | annotate |
| Fri, 18 Sep 1998 14:36:03 +0200 | paulson | theorem le_diff_conv2; tidying and expandshort | file | diff | annotate |
| Mon, 14 Sep 1998 10:17:19 +0200 | paulson | new theorem le_diff_conv | file | diff | annotate |
| Mon, 07 Sep 1998 10:40:17 +0200 | paulson | tidying | file | diff | annotate |
| Fri, 04 Sep 1998 11:01:59 +0200 | nipkow | Arith: less_diff_conv | file | diff | annotate |
| 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) | file | diff | annotate |
| Tue, 01 Sep 1998 10:09:11 +0200 | paulson | Two new subtraction lemmas | file | diff | annotate |
| Thu, 20 Aug 1998 16:58:28 +0200 | paulson | new theorems | file | diff | annotate |
| Wed, 19 Aug 1998 10:26:02 +0200 | paulson | Some new theorems. zero_less_diff replaces less_imp_diff_positive | file | diff | annotate |
| Tue, 18 Aug 1998 10:24:09 +0200 | paulson | new theorem diff_Suc_less_diff | file | diff | annotate |
| Thu, 13 Aug 1998 18:14:26 +0200 | paulson | even more tidying of Goal commands | file | diff | annotate |
| Thu, 06 Aug 1998 12:45:02 +0200 | nipkow | Removed duplicate thms: | file | diff | annotate |
| Fri, 24 Jul 1998 13:03:20 +0200 | berghofe | Adapted to new datatype package. | file | diff | annotate |
| Wed, 15 Jul 1998 10:15:13 +0200 | paulson | Removal of leading "\!\!..." from most Goal commands | file | diff | annotate |
| Thu, 25 Jun 1998 13:57:34 +0200 | paulson | Installation of target HOL-Real | file | diff | annotate |
| Mon, 22 Jun 1998 17:26:46 +0200 | wenzelm | isatool fixgoal; | file | diff | annotate |
| Mon, 27 Apr 1998 16:45:11 +0200 | nipkow | Added a few lemmas. | file | diff | annotate |
| Thu, 12 Mar 1998 10:37:58 +0100 | paulson | New laws, mostly generalizing old "pred" ones | file | diff | annotate |
| Wed, 11 Mar 1998 11:03:43 +0100 | paulson | Arith.thy -> thy; proved a few new theorems | file | diff | annotate |
| Sat, 07 Mar 1998 16:29:29 +0100 | nipkow | Removed `addsplits [expand_if]' | file | diff | annotate |
| Tue, 03 Mar 1998 15:11:26 +0100 | paulson | New theorem diff_Suc_le_Suc_diff; tidied another proof | file | diff | annotate |
| Tue, 16 Dec 1997 17:58:03 +0100 | wenzelm | expandshort; | file | diff | annotate |