src/HOL/Analysis/Bochner_Integration.thy
5 months ago nipkow 2019-01-25 tuned
5 months ago Angeliki KoutsoukouArgyraki 2019-01-22 minor tagging updates in 13 theories
5 months ago paulson 2019-01-21 new material about summations and powers, along with some tweaks
5 months ago immler 2019-01-17 subsection is always %important
5 months ago Angeliki KoutsoukouArgyraki 2019-01-14 updated tagging first 5
5 months ago wenzelm 2019-01-05 isabelle update -u control_cartouches;
5 months ago wenzelm 2019-01-01 more antiquotations -- less LaTeX macros;
5 months ago haftmann 2018-12-30 prefer naming convention from datatype package for strong congruence rules
8 months ago paulson 2018-10-17 new theory Abstract_Topology with lots of stuff from HOL Light's metric.sml
9 months ago nipkow 2018-09-24 Prefix form of infix with * on either side no longer needs special treatment because (* and *) are no longer comment brackets in terms.
10 months ago Angeliki KoutsoukouArgyraki 2018-08-28 tagged 21 theories in the Analysis library for the manual
10 months ago nipkow 2018-08-24 tuned proofs
10 months ago nipkow 2018-08-23 moved lemma from AFP
12 months ago nipkow 2018-06-06 reorient -> split; documented split
13 months ago immler 2018-05-03 merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
13 months ago immler 2018-05-02 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
14 months ago nipkow 2018-04-26 new simp modifier: reorient
17 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
20 months ago haftmann 2017-10-08 avoid name clashes on interpretation of abstract locales
22 months ago eberlm 2017-08-17 Replaced subseq with strict_mono
2017-05-02 paulson 2017-05-02 Simplification of some proofs. Also key lemmas using !! rather than ! in premises
2017-01-17 wenzelm 2017-01-17 isabelle update_cartouches -c -t;
2016-10-18 paulson 2016-10-18 more from moretop.ml
2016-10-13 hoelzl 2016-10-13 HOL-Probability: move conditional expectation from AFP/Ergodic_Theory
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-09-30 hoelzl 2016-09-30 HOL-Probability: more about probability, prepare for Markov processes in the AFP
2016-09-23 hoelzl 2016-09-23 move absolutely_integrable_on to Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral
2016-09-16 hoelzl 2016-09-16 move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
2016-08-08 hoelzl 2016-08-08 rename HOL-Multivariate_Analysis to HOL-Analysis.