src/HOL/Library/FuncSet.thy
13 months ago wenzelm 2018-05-15 tuned headers;
13 months ago immler 2018-05-15 move FuncSet back to HOL-Library (amending 493b818e8e10)
19 months ago wenzelm 2017-11-05 more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
19 months ago wenzelm 2017-11-04 prefer main entry points of HOL;
22 months ago wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2017-01-17 wenzelm 2017-01-17 removed some old ASCII syntax;
2017-01-17 wenzelm 2017-01-17 more symbols via abbrevs;
2016-05-13 wenzelm 2016-05-13 eliminated use of empty "assms";
2016-04-26 wenzelm 2016-04-26 some uses of 'obtain' with structure statement;
2016-02-23 nipkow 2016-02-23 more canonical names
2015-12-28 wenzelm 2015-12-28 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
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