| 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 |
| 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 |
| 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 |