| Fri, 23 Oct 1998 22:37:15 +0200 | berghofe | Added theorem bool_induct (for rep_datatype). | file | diff | annotate |
| Fri, 09 Oct 1998 11:27:11 +0200 | paulson | new theorem | file | diff | annotate |
| Thu, 01 Oct 1998 18:22:24 +0200 | paulson | white space | file | diff | annotate |
| Mon, 21 Sep 1998 23:12:31 +0200 | oheimb | added wrapper for bspec | file | diff | annotate |
| Tue, 15 Sep 1998 15:04:07 +0200 | paulson | From Compl(A) to -A | file | diff | annotate |
| Tue, 18 Aug 1998 10:25:13 +0200 | paulson | new theorem Un_Diff_Int | file | diff | annotate |
| Fri, 14 Aug 1998 12:06:34 +0200 | paulson | Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML | file | diff | annotate |
| Thu, 13 Aug 1998 18:14:26 +0200 | paulson | even more tidying of Goal commands | file | diff | annotate |
| Sat, 08 Aug 1998 14:00:56 +0200 | nipkow | List now contains some lexicographic orderings. | file | diff | annotate |
| Thu, 06 Aug 1998 15:48:13 +0200 | paulson | even more tidying of Goal commands | file | diff | annotate |
| Tue, 04 Aug 1998 10:48:21 +0200 | paulson | Boolean quantification | file | diff | annotate |
| Mon, 03 Aug 1998 10:36:39 +0200 | paulson | New rewrite rules for quantification over bounded UNIONs | file | diff | annotate |
| Fri, 24 Jul 1998 13:35:47 +0200 | berghofe | Added theorem distinct_lemma (needed for datatypes). | file | diff | annotate |
| Wed, 15 Jul 1998 14:19:02 +0200 | paulson | More tidying and removal of "\!\!... from Goal commands | 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 |
| Fri, 01 May 1998 22:27:43 +0200 | oheimb | added insert_Collect | file | diff | annotate |
| Thu, 02 Apr 1998 13:49:04 +0200 | paulson | new theorems | file | diff | annotate |
| Mon, 23 Mar 1998 13:56:53 +0100 | paulson | more thms | file | diff | annotate |
| Sat, 07 Mar 1998 16:29:29 +0100 | nipkow | Removed `addsplits [expand_if]' | file | diff | annotate |
| Tue, 03 Mar 1998 15:12:57 +0100 | paulson | New theorems | file | diff | annotate |
| Fri, 27 Feb 1998 11:07:58 +0100 | paulson | New absorbsion laws, etc | file | diff | annotate |
| Mon, 23 Feb 1998 11:16:18 +0100 | paulson | New laws for union | file | diff | annotate |
| Thu, 19 Feb 1998 15:01:25 +0100 | paulson | Four new Union/Intersection laws | file | diff | annotate |
| Tue, 10 Feb 1998 10:27:30 +0100 | paulson | New Addsimps for Compl rules | file | diff | annotate |
| Sat, 07 Feb 1998 14:38:57 +0100 | paulson | AC and other rewrite rules for Un and Int | file | diff | annotate |
| Fri, 06 Feb 1998 18:55:18 +0100 | nipkow | Added `remdups' | 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 |
| Wed, 26 Nov 1997 17:32:52 +0100 | paulson | Tidying and using equalityCE instead of the slower equalityE | file | diff | annotate |