src/HOL/Library/FuncSet.thy
Fri, 09 Oct 2015 20:26:03 +0200 wenzelm discontinued specific HTML syntax;
Wed, 07 Oct 2015 17:11:16 +0200 hoelzl cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
Thu, 22 Jan 2015 14:51:08 +0100 hoelzl import general thms from Density_Compiler
Sun, 02 Nov 2014 17:20:45 +0100 wenzelm modernized header;
Sat, 25 Oct 2014 21:16:32 +0200 wenzelm tuned whitespace;
Tue, 07 Oct 2014 10:34:24 +0200 hoelzl add Giry monad
Mon, 28 Apr 2014 17:50:03 +0200 wenzelm tuned;
Tue, 12 Nov 2013 19:28:56 +0100 hoelzl add restrict_space measure
Tue, 03 Sep 2013 22:04:23 +0200 wenzelm tuned proofs -- less guessing;
Tue, 13 Aug 2013 16:25:47 +0200 wenzelm standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
Mon, 19 Nov 2012 12:29:02 +0100 hoelzl merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
Fri, 16 Nov 2012 18:45:57 +0100 hoelzl move theorems to be more generally useable
Wed, 25 Apr 2012 19:26:00 +0200 hoelzl moved lemmas to appropriate places
Mon, 22 Aug 2011 20:11:44 +0200 wenzelm reduced warnings;
Mon, 22 Nov 2010 10:41:51 +0100 bulwahn adding extensional function spaces to the FuncSet library theory
Mon, 20 Sep 2010 21:09:25 +0200 nipkow new lemmas
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Mon, 23 Aug 2010 19:35:57 +0200 hoelzl Rewrite the Probability theory.
Wed, 28 Oct 2009 11:42:31 +0000 paulson New theory Probability, which contains a development of measure theory
Thu, 22 Oct 2009 09:27:48 +0200 nipkow inv_onto -> inv_into
Sun, 18 Oct 2009 12:07:25 +0200 nipkow Inv -> inv_onto, inv abbr. inv_onto UNIV.
Tue, 23 Jun 2009 11:32:12 +0200 haftmann merged
Tue, 23 Jun 2009 11:31:28 +0200 haftmann lemma funcset_id by Jeremy Avigad
Tue, 23 Jun 2009 05:57:35 +0200 nipkow fixed name
Mon, 22 Jun 2009 20:59:12 +0200 nipkow tuned FuncSet
Sat, 20 Jun 2009 14:00:36 +0200 nipkow tuned
Fri, 19 Jun 2009 22:49:12 +0200 nipkow Made Pi_I [simp]
Mon, 23 Mar 2009 08:14:24 +0100 haftmann Main is (Complex_Main) base entry point in library theories
Tue, 07 Oct 2008 16:07:50 +0200 haftmann arbitrary is undefined
Mon, 07 Jul 2008 08:47:17 +0200 haftmann absolute imports of HOL/*.thy theories
Thu, 26 Jun 2008 10:07:01 +0200 haftmann established Plain theory and image
Thu, 12 Jun 2008 22:29:50 +0200 wenzelm removed obsolete skolem declarations -- done by Theory.at_end;
Thu, 21 Feb 2008 17:34:09 +0100 nipkow moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Tue, 07 Nov 2006 11:47:57 +0100 wenzelm renamed 'const_syntax' to 'notation';
Thu, 28 Sep 2006 23:42:43 +0200 wenzelm fixed translations: CONST;
Tue, 08 Aug 2006 18:40:56 +0200 paulson skolem declarations for built-in theorems
Sat, 27 May 2006 17:42:02 +0200 wenzelm tuned;
Tue, 16 May 2006 21:33:01 +0200 wenzelm tuned concrete syntax -- abbreviation/const_syntax;
Tue, 02 May 2006 20:42:32 +0200 wenzelm replaced syntax/translations by abbreviation;
Fri, 07 Oct 2005 22:59:18 +0200 wenzelm print_translation: does not handle _idtdummy;
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
Tue, 01 Jun 2004 11:25:26 +0200 paulson more on bij_betw
Wed, 19 May 2004 11:30:56 +0200 paulson new bij_betw operator
Fri, 14 May 2004 16:49:42 +0200 paulson new lemmas
Thu, 06 May 2004 14:14:18 +0200 wenzelm tuned document;
Wed, 14 Apr 2004 14:13:05 +0200 kleing use more symbols in HTML output
Fri, 27 Sep 2002 16:44:50 +0200 paulson Proof tidying
Fri, 27 Sep 2002 10:36:21 +0200 paulson Tidied. New Pi-theorem.
Thu, 26 Sep 2002 10:51:58 +0200 paulson new theory for Pi-sets, restrict, etc.
less more (0) tip