src/ZF/func.thy
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