Sun, 23 Apr 2000 11:39:32 +0200 |
paulson |
this change saves 15 seconds
|
file |
diff |
annotate
|
Mon, 28 Feb 2000 10:48:39 +0100 |
paulson |
more bijection theorems
|
file |
diff |
annotate
|
Wed, 23 Feb 2000 10:43:02 +0100 |
paulson |
new theorems inj_iff, surj_iff
|
file |
diff |
annotate
|
Fri, 18 Feb 2000 20:24:16 +0100 |
oheimb |
changed precedence of function update
|
file |
diff |
annotate
|
Fri, 18 Feb 2000 15:33:09 +0100 |
paulson |
many new theorems about inj, surj etc.
|
file |
diff |
annotate
|
Thu, 10 Feb 2000 11:08:42 +0100 |
paulson |
new thm and simprule inv_id
|
file |
diff |
annotate
|
Mon, 31 Jan 2000 16:18:09 +0100 |
paulson |
various theorems about image and inverse image
|
file |
diff |
annotate
|
Fri, 28 Jan 2000 14:07:53 +0100 |
oheimb |
added inj_singleton
|
file |
diff |
annotate
|
Fri, 21 Jan 2000 10:45:40 +0100 |
paulson |
new theorem inj_on_restrict_eq
|
file |
diff |
annotate
|
Thu, 23 Dec 1999 19:59:50 +0100 |
oheimb |
removed inj_eq from the default simpset again
|
file |
diff |
annotate
|
Wed, 27 Oct 1999 19:32:19 +0200 |
oheimb |
added various little lemmas
|
file |
diff |
annotate
|
Fri, 22 Oct 1999 18:41:00 +0200 |
paulson |
replaced image_image_eq_UN by image_eq_UN
|
file |
diff |
annotate
|
Mon, 18 Oct 1999 15:16:10 +0200 |
paulson |
new thm vimage_image_eq
|
file |
diff |
annotate
|
Fri, 10 Sep 1999 18:37:04 +0200 |
paulson |
new theorem image_image_eq_UN
|
file |
diff |
annotate
|
Wed, 08 Sep 1999 15:38:12 +0200 |
paulson |
images and preimages of the identity function
|
file |
diff |
annotate
|
Fri, 03 Sep 1999 10:14:28 +0200 |
paulson |
new theorem fun_upd_upd
|
file |
diff |
annotate
|
Fri, 27 Aug 1999 15:41:11 +0200 |
paulson |
the bij predicate (at last)
|
file |
diff |
annotate
|
Wed, 25 Aug 1999 10:45:41 +0200 |
paulson |
new theorem inv_f_eq
|
file |
diff |
annotate
|
Tue, 27 Jul 1999 17:19:31 +0200 |
paulson |
expandshort and tidying
|
file |
diff |
annotate
|
Wed, 21 Jul 1999 11:34:59 +0200 |
nipkow |
Mod by Norber Voelcker
|
file |
diff |
annotate
|
Fri, 16 Jul 1999 12:09:48 +0200 |
berghofe |
Added some definitions and theorems needed for the
|
file |
diff |
annotate
|
Thu, 17 Jun 1999 10:32:52 +0200 |
paulson |
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
|
file |
diff |
annotate
|
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
|