src/HOL/Fun.thy
2006-03-23 nipkow 2006-03-23 Converted translations to abbbreviations. Removed a few odd functions from Map and AssocList. Moved chg_map from Map to Bali/Basis.
2005-11-11 huffman 2005-11-11 add header
2005-10-21 wenzelm 2005-10-21 Goal.prove;
2005-10-17 wenzelm 2005-10-17 Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-09-22 nipkow 2005-09-22 renamed rules to iprover
2005-08-16 paulson 2005-08-16 classical rules must have names for ATP integration
2005-08-01 wenzelm 2005-08-01 simprocs: Simplifier.inherit_bounds;
2005-07-07 nipkow 2005-07-07 linear arithmetic now takes "&" in assumptions apart.
2005-04-10 nipkow 2005-04-10 _(_|_) is now override_on
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-02-09 paulson 2005-02-09 new foldSet proofs
2005-01-14 nipkow 2005-01-14 made diff_less a simp rule
2004-11-21 nipkow 2004-11-21 added lemmas
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-08-04 nipkow 2004-08-04 added some inj_on thms
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2003-04-14 nipkow 2003-04-14 Added thms
2002-10-10 berghofe 2002-10-10 - Added range_ex1_eq - Removed obsolete theorems inj_o and inj_fun_lemma
2002-09-26 paulson 2002-09-26 Converted Fun to Isar style. Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy. Renamed constant "Fun.op o" to "Fun.comp"
2001-12-11 wenzelm 2001-12-11 oops;
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-11-21 wenzelm 2001-11-21 got rid of theory Inverse_Image;
2001-11-09 wenzelm 2001-11-09 eliminated old "symbols" syntax, use "xsymbols" instead;
2001-09-27 wenzelm 2001-09-27 eliminated theories "equalities" and "mono" (made part of "Typedef", which supercedes "subset");
2001-07-25 paulson 2001-07-25 partial restructuring to reduce dependence on Axiom of Choice
2001-02-14 oheimb 2001-02-14 removed whitespace
2001-01-08 nipkow 2001-01-08 Removed Applyall
2000-10-12 nipkow 2000-10-12 *** empty log message ***
2000-07-16 wenzelm 2000-07-16 syntax (symbols) "op o" moved from HOL to Fun;
2000-07-14 oheimb 2000-07-14 added hint on fun_sum
2000-07-13 wenzelm 2000-07-13 fixed compose decl;
2000-06-25 wenzelm 2000-06-25 tuned;
2000-05-24 paulson 2000-05-24 we must not require SetInterval this early
2000-05-23 nipkow 2000-05-23 Added SetInterval
2000-02-18 oheimb 2000-02-18 changed precedence of function update
1999-08-27 paulson 1999-08-27 the bij predicate (at last)
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