| Wed, 07 Jun 2000 12:06:36 +0200 | paulson | tidied | file | diff | annotate |
| Tue, 23 May 2000 18:06:22 +0200 | paulson | added type constraint ::nat because 0 is now overloaded | file | diff | annotate |
| Fri, 12 May 2000 14:59:12 +0200 | paulson | deleted some redundant simprules | file | diff | annotate |
| Mon, 08 May 2000 16:58:18 +0200 | paulson | moved le_square, proved le_cube | file | diff | annotate |
| Tue, 18 Apr 2000 15:56:41 +0200 | paulson | replaced obsolete diff_right_cancel by diff_diff_eq | file | diff | annotate |
| Thu, 13 Apr 2000 15:18:02 +0200 | paulson | added some new iff-lemmas; removed some obsolete thms | file | diff | annotate |
| Fri, 24 Mar 2000 20:59:15 +0100 | wenzelm | arith method: HEADGOAL; | file | diff | annotate |
| Fri, 17 Mar 2000 17:11:59 +0100 | wenzelm | arith method: bang arg; | file | diff | annotate |
| 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 |