src/HOL/Fun.ML
2000-06-22 wenzelm 2000-06-22 bind_thm(s);
2000-04-23 paulson 2000-04-23 this change saves 15 seconds
2000-02-28 paulson 2000-02-28 more bijection theorems
2000-02-23 paulson 2000-02-23 new theorems inj_iff, surj_iff
2000-02-18 oheimb 2000-02-18 changed precedence of function update
2000-02-18 paulson 2000-02-18 many new theorems about inj, surj etc.
2000-02-10 paulson 2000-02-10 new thm and simprule inv_id
2000-01-31 paulson 2000-01-31 various theorems about image and inverse image
2000-01-28 oheimb 2000-01-28 added inj_singleton
2000-01-21 paulson 2000-01-21 new theorem inj_on_restrict_eq
1999-12-23 oheimb 1999-12-23 removed inj_eq from the default simpset again
1999-10-27 oheimb 1999-10-27 added various little lemmas
1999-10-22 paulson 1999-10-22 replaced image_image_eq_UN by image_eq_UN
1999-10-18 paulson 1999-10-18 new thm vimage_image_eq
1999-09-10 paulson 1999-09-10 new theorem image_image_eq_UN
1999-09-08 paulson 1999-09-08 images and preimages of the identity function
1999-09-03 paulson 1999-09-03 new theorem fun_upd_upd
1999-08-27 paulson 1999-08-27 the bij predicate (at last)
1999-08-25 paulson 1999-08-25 new theorem inv_f_eq
1999-07-27 paulson 1999-07-27 expandshort and tidying
1999-07-21 nipkow 1999-07-21 Mod by Norber Voelcker
1999-07-16 berghofe 1999-07-16 Added some definitions and theorems needed for the construction of datatypes involving function types.
1999-06-17 paulson 1999-06-17 renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
1999-03-03 paulson 1999-03-03 expandshort
1999-02-22 paulson 1999-02-22 new image laws
1999-02-09 paulson 1999-02-09 new lemma surjD
1999-02-05 paulson 1999-02-05 new surj rules
1999-02-03 paulson 1999-02-03 inj is now a translation of inj_on
1998-11-16 paulson 1998-11-16 moved some facts about Pi from ex/PiSets to Fun.ML
1998-11-13 paulson 1998-11-13 the function space operator
1998-11-11 paulson 1998-11-11 proved surjI
1998-10-02 nipkow 1998-10-02 id <-> Id
1998-09-09 oheimb 1998-09-09 added Id_apply
1998-08-14 paulson 1998-08-14 expandshort
1998-08-13 paulson 1998-08-13 even more tidying of Goal commands
1998-08-12 oheimb 1998-08-12 added theorems Id_o, o_Id corrected name of theorem: fund_upd_other -> fun_upd_other
1998-08-12 oheimb 1998-08-12 cleanup for Fun.thy: merged Update.{thy|ML} into Fun.{thy|ML} moved o_def from HOL.thy to Fun.thy added Id_def to Fun.thy moved image_compose from Set.ML to Fun.ML moved o_apply and o_assoc from simpdata.ML to Fun.ML moved fun_upd_same and fun_upd_other (from Map.ML) to Fun.ML added fun_upd_twist to Fun.ML
1998-07-15 paulson 1998-07-15 More tidying and removal of "\!\!... from Goal commands
1998-07-15 paulson 1998-07-15 Removal of leading "\!\!..." from most Goal commands
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-04-27 nipkow 1998-04-27 Added a few lemmas. Renamed expand_const -> split_const.
1998-02-26 paulson 1998-02-26 Proved choice and bchoice; changed Fun.thy -> thy
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-11-01 paulson 1997-11-01 New Blast_tac (and minor tidying...)
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-05-26 paulson 1997-05-26 New theorem subset_inj_onto
1997-04-11 paulson 1997-04-11 Yet more fast_tac->blast_tac, and other tidying
1997-04-09 paulson 1997-04-09 Using Blast_tac
1997-04-04 nipkow 1997-04-04 moved inj and surj from Set to Fun and Inv -> inv.
1997-04-04 paulson 1997-04-04 Adds image_eqI instead of imageI, as the former is more general
1997-01-09 paulson 1997-01-09 Tidying of proofs. New theorems are enterred immediately into the relevant clasets or simpsets.
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-07-26 paulson 1996-07-26 Redefining "range" as a macro
1996-06-28 paulson 1996-06-28 Now set_cs is just taken from !claset
1996-06-21 berghofe 1996-06-21 Replaced occurrence of set_cs by claset_of "Fun" .
1996-05-31 oheimb 1996-05-31 moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML, as there have been unnecessary proofs of anonymous thms, which could not be removed (by name) from the !simpset where necessary. All these thms except singleton_iff were already proved in Set.ML. therefore in Set.ML: New version of singletonE, proof of new thm singleton_iff
1996-05-21 berghofe 1996-05-21 Replaced fast_tac by Fast_tac (which uses default claset) New rules are now also added to default claset.
1996-04-23 oheimb 1996-04-23 repaired critical proofs depending on the order inside non-confluent SimpSets, (temporarily) removed problematic rule less_Suc_eq form simpset_of "Nat"
1996-04-19 clasohm 1996-04-19 removed assignment of HOL_ss to simpset
1996-03-11 paulson 1996-03-11 set_cs now includes singleton_inject