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
|