src/ZF/func.thy
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-11-01 wenzelm 2014-11-01 eliminated spurious semicolons;
2012-03-15 paulson 2012-03-15 replacing ":" by "\<in>"
2012-03-06 paulson 2012-03-06 Using mathematical notation for <-> and cardinal arithmetic
2012-03-06 paulson 2012-03-06 mathematical symbols instead of ASCII
2010-12-17 wenzelm 2010-12-17 replaced command 'nonterminals' by slightly modernized version 'nonterminal';
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2008-07-29 ballarin 2008-07-29 Lemmas added
2008-06-11 wenzelm 2008-06-11 tuned comments;
2007-10-07 wenzelm 2007-10-07 modernized specifications; removed legacy ML bindings;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-06-08 paulson 2004-06-08 Groups, Rings and supporting lemmas
2003-08-19 paulson 2003-08-19 new case_tac
2003-07-10 paulson 2003-07-10 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new variable
2003-05-27 paulson 2003-05-27 updating ZF-UNITY with Sidi's new material
2002-10-01 paulson 2002-10-01 Numerous cosmetic changes, prompted by the new simplifier
2002-07-14 paulson 2002-07-14 Removal of mono.thy
2002-07-14 paulson 2002-07-14 merged Update with func
2002-07-02 paulson 2002-07-02 Tidying and introduction of various new theorems
2002-06-26 paulson 2002-06-26 new theorems
2002-06-19 paulson 2002-06-19 conversion of Cardinal, CardinalArith
2002-06-18 paulson 2002-06-18 new lemma
2002-05-24 paulson 2002-05-24 strong lemmas about functions
2002-05-24 paulson 2002-05-24 conversion of Perm to Isar. Strengthening of comp_fun_apply
2002-05-23 paulson 2002-05-23 new definition of "apply" and new simprule "beta_if"
2002-05-22 paulson 2002-05-22 more tidying
2002-05-22 paulson 2002-05-22 tidying up
2002-05-21 paulson 2002-05-21 converted domrange to Isar and merged with equalities
2002-05-18 paulson 2002-05-18 converted Arith, Univ, func to Isar format!
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF
1994-08-15 lcp 1994-08-15 ZF/func/empty_fun: renamed from fun_empty ZF/func/single_fun: replaces the weaker fun_single ZF/func/fun_single_lemma: deleted ZF/func.thy: now depends upon equalities.thy
1993-11-16 clasohm 1993-11-16 made pseudo theories for all ML files; documented dependencies between all thy and ML files