src/HOL/Library/FuncSet.thy
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-10-10 wenzelm 2015-10-10 prefer symbols;
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-10-07 hoelzl 2015-10-07 cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
2015-01-22 hoelzl 2015-01-22 import general thms from Density_Compiler
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-25 wenzelm 2014-10-25 tuned whitespace; more symbols;
2014-10-07 hoelzl 2014-10-07 add Giry monad
2014-04-28 wenzelm 2014-04-28 tuned;
2013-11-12 hoelzl 2013-11-12 add restrict_space measure
2013-09-03 wenzelm 2013-09-03 tuned proofs -- less guessing;
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2012-11-19 hoelzl 2012-11-19 merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
2012-11-16 hoelzl 2012-11-16 move theorems to be more generally useable
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.