src/HOL/Fun.thy
1999-02-03 paulson 1999-02-03 inj is now a translation of inj_on
1998-11-13 paulson 1998-11-13 the function space operator
1998-10-02 nipkow 1998-10-02 id <-> Id
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-04-27 nipkow 1998-04-27 Added a few lemmas. Renamed expand_const -> split_const.
1998-02-24 paulson 1998-02-24 New theory of the inverse image of a function
1997-11-01 paulson 1997-11-01 New Blast_tac (and minor tidying...)
1997-04-04 nipkow 1997-04-04 moved inj and surj from Set to Fun and Inv -> inv.
1996-02-05 clasohm 1996-02-05 expanded tabs; renamed subtype to typedef; incorporated Konrad's changes
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application