src/HOL/Fun.ML
Sun, 23 Apr 2000 11:39:32 +0200 paulson this change saves 15 seconds
Mon, 28 Feb 2000 10:48:39 +0100 paulson more bijection theorems
Wed, 23 Feb 2000 10:43:02 +0100 paulson new theorems inj_iff, surj_iff
Fri, 18 Feb 2000 20:24:16 +0100 oheimb changed precedence of function update
Fri, 18 Feb 2000 15:33:09 +0100 paulson many new theorems about inj, surj etc.
Thu, 10 Feb 2000 11:08:42 +0100 paulson new thm and simprule inv_id
Mon, 31 Jan 2000 16:18:09 +0100 paulson various theorems about image and inverse image
Fri, 28 Jan 2000 14:07:53 +0100 oheimb added inj_singleton
Fri, 21 Jan 2000 10:45:40 +0100 paulson new theorem inj_on_restrict_eq
Thu, 23 Dec 1999 19:59:50 +0100 oheimb removed inj_eq from the default simpset again
Wed, 27 Oct 1999 19:32:19 +0200 oheimb added various little lemmas
Fri, 22 Oct 1999 18:41:00 +0200 paulson replaced image_image_eq_UN by image_eq_UN
Mon, 18 Oct 1999 15:16:10 +0200 paulson new thm vimage_image_eq
Fri, 10 Sep 1999 18:37:04 +0200 paulson new theorem image_image_eq_UN
Wed, 08 Sep 1999 15:38:12 +0200 paulson images and preimages of the identity function
Fri, 03 Sep 1999 10:14:28 +0200 paulson new theorem fun_upd_upd
Fri, 27 Aug 1999 15:41:11 +0200 paulson the bij predicate (at last)
Wed, 25 Aug 1999 10:45:41 +0200 paulson new theorem inv_f_eq
Tue, 27 Jul 1999 17:19:31 +0200 paulson expandshort and tidying
Wed, 21 Jul 1999 11:34:59 +0200 nipkow Mod by Norber Voelcker
Fri, 16 Jul 1999 12:09:48 +0200 berghofe Added some definitions and theorems needed for the
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
Wed, 03 Mar 1999 11:15:18 +0100 paulson expandshort
Mon, 22 Feb 1999 10:21:59 +0100 paulson new image laws
Tue, 09 Feb 1999 10:45:55 +0100 paulson new lemma surjD
Fri, 05 Feb 1999 17:31:04 +0100 paulson new surj rules
Wed, 03 Feb 1999 13:26:07 +0100 paulson inj is now a translation of inj_on
Mon, 16 Nov 1998 10:36:30 +0100 paulson moved some facts about Pi from ex/PiSets to Fun.ML
Fri, 13 Nov 1998 13:26:16 +0100 paulson the function space operator
Wed, 11 Nov 1998 15:49:15 +0100 paulson proved surjI
Fri, 02 Oct 1998 14:28:39 +0200 nipkow id <-> Id
Wed, 09 Sep 1998 16:43:14 +0200 oheimb added Id_apply
Fri, 14 Aug 1998 12:03:01 +0200 paulson expandshort
Thu, 13 Aug 1998 18:14:26 +0200 paulson even more tidying of Goal commands
Wed, 12 Aug 1998 16:49:25 +0200 oheimb added theorems Id_o, o_Id
Wed, 12 Aug 1998 16:23:25 +0200 oheimb cleanup for Fun.thy:
Wed, 15 Jul 1998 14:19:02 +0200 paulson More tidying and removal of "\!\!... from Goal commands
Wed, 15 Jul 1998 10:15:13 +0200 paulson Removal of leading "\!\!..." from most Goal commands
Mon, 22 Jun 1998 17:26:46 +0200 wenzelm isatool fixgoal;
Mon, 27 Apr 1998 16:45:11 +0200 nipkow Added a few lemmas.
Thu, 26 Feb 1998 11:07:37 +0100 paulson Proved choice and bchoice; changed Fun.thy -> thy
Mon, 03 Nov 1997 12:13:18 +0100 wenzelm isatool fixclasimp;
Sat, 01 Nov 1997 12:59:06 +0100 paulson New Blast_tac (and minor tidying...)
Fri, 10 Oct 1997 19:02:28 +0200 wenzelm fixed dots;
Mon, 26 May 1997 12:37:24 +0200 paulson New theorem subset_inj_onto
Fri, 11 Apr 1997 15:21:36 +0200 paulson Yet more fast_tac->blast_tac, and other tidying
Wed, 09 Apr 1997 12:32:04 +0200 paulson Using Blast_tac
Fri, 04 Apr 1997 16:33:28 +0200 nipkow moved inj and surj from Set to Fun and Inv -> inv.
Fri, 04 Apr 1997 11:18:19 +0200 paulson Adds image_eqI instead of imageI, as the former is more general
Thu, 09 Jan 1997 10:23:39 +0100 paulson Tidying of proofs. New theorems are enterred immediately into the
Thu, 26 Sep 1996 12:47:47 +0200 paulson Ran expandshort
Fri, 26 Jul 1996 12:17:04 +0200 paulson Redefining "range" as a macro
Fri, 28 Jun 1996 11:16:12 +0200 paulson Now set_cs is just taken from !claset
Fri, 21 Jun 1996 13:39:08 +0200 berghofe Replaced occurrence of set_cs by claset_of "Fun" .
Fri, 31 May 1996 19:12:00 +0200 oheimb moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
Tue, 21 May 1996 13:39:31 +0200 berghofe Replaced fast_tac by Fast_tac (which uses default claset)
Tue, 23 Apr 1996 16:58:21 +0200 oheimb repaired critical proofs depending on the order inside non-confluent SimpSets,
Fri, 19 Apr 1996 11:13:05 +0200 clasohm removed assignment of HOL_ss to simpset
Mon, 11 Mar 1996 14:04:37 +0100 paulson set_cs now includes singleton_inject
Tue, 30 Jan 1996 15:24:36 +0100 clasohm expanded tabs
less more (0) -60 tip