| Thu, 12 Oct 2000 18:38:23 +0200 | nipkow | *** empty log message *** | file | diff | annotate |
| Sun, 16 Jul 2000 20:48:35 +0200 | wenzelm | syntax (symbols) "op o" moved from HOL to Fun; | file | diff | annotate |
| Fri, 14 Jul 2000 16:27:45 +0200 | oheimb | added hint on fun_sum | file | diff | annotate |
| Thu, 13 Jul 2000 23:08:42 +0200 | wenzelm | fixed compose decl; | file | diff | annotate |
| Sun, 25 Jun 2000 23:58:27 +0200 | wenzelm | tuned; | file | diff | annotate |
| Wed, 24 May 2000 18:48:03 +0200 | paulson | we must not require SetInterval this early | file | diff | annotate |
| Tue, 23 May 2000 07:32:24 +0200 | nipkow | Added SetInterval | file | diff | annotate |
| Fri, 18 Feb 2000 20:24:16 +0100 | oheimb | changed precedence of function update | file | diff | annotate |
| Fri, 27 Aug 1999 15:41:11 +0200 | paulson | the bij predicate (at last) | file | diff | annotate |
| Wed, 03 Feb 1999 13:26:07 +0100 | paulson | inj is now a translation of inj_on | file | diff | annotate |
| Fri, 13 Nov 1998 13:26:16 +0100 | paulson | the function space operator | file | diff | annotate |
| Fri, 02 Oct 1998 14:28:39 +0200 | nipkow | id <-> Id | file | diff | annotate |
| Wed, 12 Aug 1998 16:23:25 +0200 | oheimb | cleanup for Fun.thy: | file | diff | annotate |
| Mon, 27 Apr 1998 16:45:11 +0200 | nipkow | Added a few lemmas. | file | diff | annotate |
| Tue, 24 Feb 1998 11:35:33 +0100 | paulson | New theory of the inverse image of a function | file | diff | annotate |
| Sat, 01 Nov 1997 12:59:06 +0100 | paulson | New Blast_tac (and minor tidying...) | 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 |
| Mon, 05 Feb 1996 21:27:16 +0100 | clasohm | expanded tabs; renamed subtype to typedef; | file | diff | annotate |
| Fri, 03 Mar 1995 12:02:25 +0100 | clasohm | new version of HOL with curried function application | file | diff | annotate |