| Wed, 23 Sep 1998 10:12:01 +0200 | paulson | deleted needless parentheses | file | diff | annotate |
| Mon, 21 Sep 1998 15:58:27 +0200 | oheimb | added indentation | file | diff | annotate |
| Fri, 11 Sep 1998 14:09:46 +0200 | oheimb | stabilized proof of card_mono | file | diff | annotate |
| Fri, 11 Sep 1998 12:55:40 +0200 | oheimb | corrected indentation | file | diff | annotate |
| Tue, 01 Sep 1998 15:04:28 +0200 | paulson | New law card_Un_Int. Removed card_insert from simpset | file | diff | annotate |
| Tue, 01 Sep 1998 10:25:05 +0200 | paulson | New lemmas involving Int | 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 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 |
| Mon, 27 Apr 1998 16:45:11 +0200 | nipkow | Added a few lemmas. | file | diff | annotate |
| Fri, 03 Apr 1998 11:22:51 +0200 | paulson | Tidied proofs | file | diff | annotate |
| Thu, 02 Apr 1998 13:47:03 +0200 | paulson | New theorems card_Diff_le and card_insert_le; tidied | file | diff | annotate |
| Mon, 30 Mar 1998 21:09:46 +0200 | oheimb | adapted proof of finite_converse | file | diff | annotate |
| Mon, 16 Mar 1998 16:50:50 +0100 | paulson | inverse -> converse | 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:29:22 +0100 | paulson | Tidied proof of finite_subset_induct | file | diff | annotate |
| Wed, 26 Nov 1997 17:27:34 +0100 | paulson | Tidying | file | diff | annotate |
| Wed, 05 Nov 1997 13:23:46 +0100 | paulson | Ran expandshort, especially to introduce Safe_tac | 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 |
| Tue, 28 Oct 1997 14:03:25 +0100 | nipkow | Added finite_UNION/SigmaI. | file | diff | annotate |
| Fri, 17 Oct 1997 15:25:12 +0200 | nipkow | setloop split_tac -> addsplits | file | diff | annotate |
| Fri, 17 Oct 1997 10:58:44 +0200 | paulson | Better simplification eliminates a command from proof of psubset_card | file | diff | annotate |
| Fri, 10 Oct 1997 19:02:28 +0200 | wenzelm | fixed dots; | file | diff | annotate |
| Mon, 29 Sep 1997 11:37:02 +0200 | paulson | Step_tac -> Safe_tac | file | diff | annotate |