| Wed, 21 Jul 1999 15:26:17 +0200 | paulson | a stronger diff_less and no more le_diff_less | file | diff | annotate |
| Mon, 19 Jul 1999 15:18:16 +0200 | paulson | new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m | file | diff | annotate |
| Thu, 15 Jul 1999 10:27:54 +0200 | paulson | qed_goal -> Goal | file | diff | annotate |
| Thu, 01 Jul 1999 10:33:50 +0200 | paulson | now div and mod are overloaded; dvd is polymorphic | file | diff | annotate |
| Sat, 09 Jan 1999 15:24:11 +0100 | nipkow | Refined arith tactic. | file | diff | annotate |
| Fri, 27 Nov 1998 17:00:30 +0100 | nipkow | At last: linear arithmetic for nat! | file | diff | annotate |
| Wed, 23 Sep 1998 10:12:01 +0200 | paulson | deleted needless parentheses | file | diff | annotate |
| Fri, 18 Sep 1998 14:36:36 +0200 | paulson | tidying | file | diff | annotate |
| Tue, 01 Sep 1998 15:03:43 +0200 | paulson | tidying; moved diff_less to Arith.ML | file | diff | annotate |
| Thu, 20 Aug 1998 16:49:47 +0200 | paulson | tidied | file | diff | annotate |
| Wed, 19 Aug 1998 10:26:37 +0200 | paulson | less_imp_diff_positive is redundant with new simprule zero_less_diff | file | diff | annotate |
| Fri, 14 Aug 1998 12:03:01 +0200 | paulson | expandshort | 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 15:48:13 +0200 | paulson | even more tidying of Goal commands | 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 |
| Mon, 22 Jun 1998 17:26:46 +0200 | wenzelm | isatool fixgoal; | file | diff | annotate |
| Tue, 21 Apr 1998 10:47:58 +0200 | paulson | Renamed mod_XXX_cancel to mod_XXX_self | file | diff | annotate |
| Mon, 20 Apr 1998 10:38:30 +0200 | paulson | New laws for mod | file | diff | annotate |
| Fri, 03 Apr 1998 11:20:41 +0200 | paulson | Tidied proofs by getting rid of case_tac | file | diff | annotate |
| Sat, 07 Mar 1998 16:29:29 +0100 | nipkow | Removed `addsplits [expand_if]' | file | diff | annotate |
| Wed, 24 Dec 1997 10:02:30 +0100 | paulson | New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort | file | diff | annotate |
| Tue, 16 Dec 1997 17:58:03 +0100 | wenzelm | expandshort; | file | diff | annotate |
| Thu, 11 Dec 1997 10:28:04 +0100 | paulson | Got rid of mod2_neq_0 | file | diff | annotate |
| Thu, 04 Dec 1997 09:05:39 +0100 | nipkow | Added thm mult_div_cancel | file | diff | annotate |
| Wed, 03 Dec 1997 17:25:43 +0100 | nipkow | Replaced n ~= 0 by 0 < n | file | diff | annotate |
| Mon, 03 Nov 1997 12:13:18 +0100 | wenzelm | isatool fixclasimp; | file | diff | annotate |
| Sat, 01 Nov 1997 12:59:06 +0100 | paulson | New Blast_tac (and minor tidying...) | file | diff | annotate |
| Fri, 17 Oct 1997 15:25:12 +0200 | nipkow | setloop split_tac -> addsplits | file | diff | annotate |
| Mon, 29 Sep 1997 11:37:02 +0200 | paulson | Step_tac -> Safe_tac | file | diff | annotate |