src/HOL/Library/FuncSet.thy
2012-04-25 hoelzl 2012-04-25 moved lemmas to appropriate places
2011-08-22 wenzelm 2011-08-22 reduced warnings;
2010-11-22 bulwahn 2010-11-22 adding extensional function spaces to the FuncSet library theory
2010-09-20 nipkow 2010-09-20 new lemmas
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-08-23 hoelzl 2010-08-23 Rewrite the Probability theory. Introduced pinfreal as real numbers with infinity. Use pinfreal as value for measures. Introduces Lebesgue Measure based on the integral in Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure spaces.
2009-10-28 paulson 2009-10-28 New theory Probability, which contains a development of measure theory
2009-10-22 nipkow 2009-10-22 inv_onto -> inv_into
2009-10-18 nipkow 2009-10-18 Inv -> inv_onto, inv abbr. inv_onto UNIV.
2009-06-23 haftmann 2009-06-23 merged
2009-06-23 haftmann 2009-06-23 lemma funcset_id by Jeremy Avigad
2009-06-23 nipkow 2009-06-23 fixed name
2009-06-22 nipkow 2009-06-22 tuned FuncSet
2009-06-20 nipkow 2009-06-20 tuned
2009-06-19 nipkow 2009-06-19 Made Pi_I [simp]
2009-03-23 haftmann 2009-03-23 Main is (Complex_Main) base entry point in library theories
2008-10-07 haftmann 2008-10-07 arbitrary is undefined
2008-07-07 haftmann 2008-07-07 absolute imports of HOL/*.thy theories
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-06-12 wenzelm 2008-06-12 removed obsolete skolem declarations -- done by Theory.at_end;
2008-02-21 nipkow 2008-02-21 moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
2006-09-28 wenzelm 2006-09-28 fixed translations: CONST;
2006-08-08 paulson 2006-08-08 skolem declarations for built-in theorems
2006-05-27 wenzelm 2006-05-27 tuned;
2006-05-16 wenzelm 2006-05-16 tuned concrete syntax -- abbreviation/const_syntax;
2006-05-02 wenzelm 2006-05-02 replaced syntax/translations by abbreviation;
2005-10-07 wenzelm 2005-10-07 print_translation: does not handle _idtdummy;
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-06-01 paulson 2004-06-01 more on bij_betw
2004-05-19 paulson 2004-05-19 new bij_betw operator
2004-05-14 paulson 2004-05-14 new lemmas
2004-05-06 wenzelm 2004-05-06 tuned document;
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2002-09-27 paulson 2002-09-27 Proof tidying
2002-09-27 paulson 2002-09-27 Tidied. New Pi-theorem.
2002-09-26 paulson 2002-09-26 new theory for Pi-sets, restrict, etc.