| Thu, 27 Sep 2001 22:22:08 +0200 | wenzelm | added surjE; | file | diff | annotate |
| Mon, 06 Aug 2001 12:40:39 +0200 | paulson | new result comp_surj | file | diff | annotate |
| Wed, 25 Jul 2001 13:13:01 +0200 | paulson | partial restructuring to reduce dependence on Axiom of Choice | file | diff | annotate |
| Mon, 23 Jul 2001 17:45:54 +0200 | paulson | improved version of the Pi-theorems | file | diff | annotate |
| Tue, 03 Jul 2001 15:29:17 +0200 | paulson | better treatment of restrict (lam) | file | diff | annotate |
| Tue, 09 Jan 2001 15:22:13 +0100 | nipkow | `` -> and ``` -> `` | file | diff | annotate |
| Mon, 08 Jan 2001 12:27:36 +0100 | nipkow | Removed Applyall | file | diff | annotate |
| Tue, 26 Sep 2000 16:42:24 +0200 | paulson | removed the obsolete (and badly named) inj_select | file | diff | annotate |
| Sat, 23 Sep 2000 16:11:38 +0200 | paulson | new theorems and comment | file | diff | annotate |
| Fri, 15 Sep 2000 15:30:50 +0200 | paulson | the final renaming: selectI -> someI | file | diff | annotate |
| Fri, 15 Sep 2000 12:39:57 +0200 | paulson | renamed (most of...) the select rules | file | diff | annotate |
| Tue, 05 Sep 2000 10:13:20 +0200 | paulson | moved proof of "choice" to Tools/meson.ML | file | diff | annotate |
| Mon, 24 Jul 2000 23:51:46 +0200 | wenzelm | avoid referencing thy value; | file | diff | annotate |
| Fri, 14 Jul 2000 16:27:42 +0200 | oheimb | added fun_upd2_simproc | file | diff | annotate |
| Thu, 22 Jun 2000 23:04:34 +0200 | wenzelm | bind_thm(s); | file | diff | annotate |
| 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 |