src/HOL/Probability/Regularity.thy
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2015-12-29 wenzelm 2015-12-29 more symbols;
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-09-30 paulson 2015-09-30 real_of_nat_Suc is now a simprule
2015-07-28 paulson 2015-07-28 the Cauchy integral theorem and related material
2015-07-03 hoelzl 2015-07-03 add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
2015-04-11 paulson 2015-04-11 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
2015-01-27 hoelzl 2015-01-27 ereal: tuned proofs concerning continuity and suprema
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-09-04 hoelzl 2014-09-04 cleanup Wfrec; introduce dependent_wf/wellorder_choice
2014-04-12 nipkow 2014-04-12 made mult_pos_pos a simp rule
2014-04-11 nipkow 2014-04-11 made divide_pos_pos a simp rule
2014-03-18 haftmann 2014-03-18 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
2014-03-18 hoelzl 2014-03-18 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2013-05-25 haftmann 2013-05-25 weaker precendence of syntax for big intersection and union on sets
2013-01-31 hoelzl 2013-01-31 use order topology for extended reals
2013-01-14 hoelzl 2013-01-14 renamed countable_basis_space to second_countable_topology
2012-12-14 wenzelm 2012-12-14 updated some headers;
2012-11-27 immler 2012-11-27 based countable topological basis on Countable_Set
2012-11-27 immler 2012-11-27 qualified interpretation of sigma_algebra, to avoid name clashes
2012-11-19 hoelzl 2012-11-19 tuned: use induction rule sigma_sets_induct_disjoint
2012-11-15 immler 2012-11-15 generalized to copy of countable types instead of instantiation of nat for discrete topology
2012-11-15 immler 2012-11-15 regularity of measures, therefore: characterization of closure with infimum distance; characterize of compact sets as totally bounded; added Diagonal_Subsequence to Library; introduced (enumerable) topological basis; rational boxes as basis of ordered euclidean space; moved some lemmas upwards