src/HOL/Probability/Projective_Limit.thy
Thu, 03 Jul 2025 13:53:14 +0200 nipkow removed duplicate lemma; added the notion of the kernel of a function
Fri, 20 Sep 2024 19:51:08 +0200 wenzelm standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
Fri, 24 Sep 2021 22:23:26 +0200 wenzelm tuned proofs --- avoid 'guess';
Tue, 22 Jan 2019 12:00:16 +0000 paulson renamings and new material
Thu, 08 Nov 2018 09:11:52 +0100 haftmann removed relics of ASCII syntax for indexed big operators
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Fri, 18 Aug 2017 20:47:47 +0200 wenzelm session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
Thu, 17 Aug 2017 14:52:56 +0200 eberlm Replaced subseq with strict_mono
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Mon, 19 Sep 2016 20:06:21 +0200 fleury left_distrib ~> distrib_right, right_distrib ~> distrib_left
Thu, 15 Sep 2016 22:41:05 +0200 Lars Hupel new type for finite maps; use it in HOL-Probability
Fri, 05 Aug 2016 18:34:57 +0200 hoelzl move measure theory from HOL-Probability to HOL-Multivariate_Analysis
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Thu, 14 Apr 2016 15:48:11 +0200 hoelzl Probability: move emeasure and nn_integral from ereal to ennreal
less more (0) -14 tip