src/HOL/Fun.ML
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
Wed, 04 Oct 1995 13:10:03 +0100 clasohm added local simpsets; removed IOA from 'make test'
Fri, 03 Mar 1995 12:02:25 +0100 clasohm new version of HOL with curried function application
less more (0) tip