src/HOL/Fun.ML
2002-08-06 wenzelm 2002-08-06 sane interface for simprocs;
2002-02-13 paulson 2002-02-13 deleted some redundant 'addS*Es [equalityC*E]'s
2001-12-10 wenzelm 2001-12-10 bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-09-27 wenzelm 2001-09-27 added surjE;
2001-08-06 paulson 2001-08-06 new result comp_surj
2001-07-25 paulson 2001-07-25 partial restructuring to reduce dependence on Axiom of Choice
2001-07-23 paulson 2001-07-23 improved version of the Pi-theorems
2001-07-03 paulson 2001-07-03 better treatment of restrict (lam)
2001-01-09 nipkow 2001-01-09 `` -> and ``` -> ``
2001-01-08 nipkow 2001-01-08 Removed Applyall
2000-09-26 paulson 2000-09-26 removed the obsolete (and badly named) inj_select Added new theorems about Compl, image, bij/inj/surj
2000-09-23 paulson 2000-09-23 new theorems and comment
2000-09-15 paulson 2000-09-15 the final renaming: selectI -> someI
2000-09-15 paulson 2000-09-15 renamed (most of...) the select rules
2000-09-05 paulson 2000-09-05 moved proof of "choice" to Tools/meson.ML
2000-07-24 wenzelm 2000-07-24 avoid referencing thy value;
2000-07-14 oheimb 2000-07-14 added fun_upd2_simproc
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