| Wed, 03 Mar 1999 11:15:18 +0100 | paulson | expandshort | file | diff | annotate |
| Mon, 22 Feb 1999 10:21:59 +0100 | paulson | new image laws | file | diff | annotate |
| Tue, 09 Feb 1999 10:45:55 +0100 | paulson | new lemma surjD | file | diff | annotate |
| Fri, 05 Feb 1999 17:31:04 +0100 | paulson | new surj rules | file | diff | annotate |
| Wed, 03 Feb 1999 13:26:07 +0100 | paulson | inj is now a translation of inj_on | file | diff | annotate |
| Mon, 16 Nov 1998 10:36:30 +0100 | paulson | moved some facts about Pi from ex/PiSets to Fun.ML | file | diff | annotate |
| Fri, 13 Nov 1998 13:26:16 +0100 | paulson | the function space operator | file | diff | annotate |
| Wed, 11 Nov 1998 15:49:15 +0100 | paulson | proved surjI | file | diff | annotate |
| Fri, 02 Oct 1998 14:28:39 +0200 | nipkow | id <-> Id | file | diff | annotate |
| Wed, 09 Sep 1998 16:43:14 +0200 | oheimb | added Id_apply | 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 |
| Wed, 12 Aug 1998 16:49:25 +0200 | oheimb | added theorems Id_o, o_Id | file | diff | annotate |
| Wed, 12 Aug 1998 16:23:25 +0200 | oheimb | cleanup for Fun.thy: | 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 |
| Thu, 26 Feb 1998 11:07:37 +0100 | paulson | Proved choice and bchoice; changed Fun.thy -> thy | 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, 10 Oct 1997 19:02:28 +0200 | wenzelm | fixed dots; | file | diff | annotate |
| Mon, 26 May 1997 12:37:24 +0200 | paulson | New theorem subset_inj_onto | file | diff | annotate |
| Fri, 11 Apr 1997 15:21:36 +0200 | paulson | Yet more fast_tac->blast_tac, and other tidying | file | diff | annotate |
| Wed, 09 Apr 1997 12:32:04 +0200 | paulson | Using Blast_tac | file | diff | annotate |
| Fri, 04 Apr 1997 16:33:28 +0200 | nipkow | moved inj and surj from Set to Fun and Inv -> inv. | file | diff | annotate |
| Fri, 04 Apr 1997 11:18:19 +0200 | paulson | Adds image_eqI instead of imageI, as the former is more general | file | diff | annotate |
| Thu, 09 Jan 1997 10:23:39 +0100 | paulson | Tidying of proofs. New theorems are enterred immediately into the | file | diff | annotate |
| Thu, 26 Sep 1996 12:47:47 +0200 | paulson | Ran expandshort | file | diff | annotate |
| Fri, 26 Jul 1996 12:17:04 +0200 | paulson | Redefining "range" as a macro | file | diff | annotate |