22 months ago paulson 2017-08-28 merged
22 months ago paulson 2017-08-28 final cleanup of negligible_standard_hyperplane and other things
22 months ago paulson 2017-08-28 merged
22 months ago paulson 2017-08-28 sorted out cases in negligible_standard_hyperplane
22 months ago paulson 2017-08-28 Unscrambling continues as far as negligible_standard_hyperplane
22 months ago paulson 2017-08-28 unscrambled has_integral_restrict_open_subinterval
22 months ago paulson 2017-08-28 merged
22 months ago paulson 2017-08-28 Giant cleanup of fundamental_theorem_of_calculus_interior
22 months ago paulson 2017-08-28 work on indefinite_integral_continuous_left, etc.
22 months ago wenzelm 2017-08-28 merged
22 months ago wenzelm 2017-08-28 not ready for release;
22 months ago wenzelm 2017-08-28 updated to cygwin-20170828, which is close to Cygwin 2.8.2-1;
22 months ago nipkow 2017-08-28 merged
22 months ago nipkow 2017-08-28 added eta_expansion and its documentation.
22 months ago eberlm 2017-08-26 More material on infinite sums
22 months ago paulson 2017-08-27 merged
22 months ago paulson 2017-08-27 some tidying of division_of_nontrivial
22 months ago paulson 2017-08-27 division_of_nontrivial partial cleanup
22 months ago nipkow 2017-08-27 tuning
22 months ago nipkow 2017-08-27 tuned
22 months ago paulson 2017-08-26 merged
22 months ago paulson 2017-08-26 Elimination of some "presume"
22 months ago paulson 2017-08-26 unscrambled Henstock_lemma_part1
22 months ago nipkow 2017-08-26 merged
22 months ago nipkow 2017-08-26 tuned
22 months ago nipkow 2017-08-26 reorganized and added log-related lemmas
22 months ago paulson 2017-08-26 merged
22 months ago paulson 2017-08-26 unscrambling esp of Henstock_lemma_part1
23 months ago paulson 2017-08-25 starting to unscramble bounded_variation_absolutely_integrable_interval
22 months ago nipkow 2017-08-26 tuned proofs
23 months ago nipkow 2017-08-25 reorganization of tree lemmas; new lemmas
23 months ago paulson 2017-08-25 merged
23 months ago paulson 2017-08-25 unscrambling of integrable_alt
23 months ago paulson 2017-08-25 renamed s to S to work with previous change
23 months ago paulson 2017-08-24 merged
23 months ago paulson 2017-08-24 work on integrable_alt, etc.
23 months ago paulson 2017-08-24 tidying up has_integral'
23 months ago paulson 2017-08-24 more elimination of "guess", etc.
23 months ago nipkow 2017-08-25 Added lemmas
23 months ago haftmann 2017-08-24 swapping of theory dependency yields less pervasive syntax requiring popular symbols \<mu>, \<nu>
23 months ago haftmann 2017-08-24 more correct output syntax declaration
23 months ago nipkow 2017-08-24 tuned
23 months ago paulson 2017-08-24 Merge (non-trivial)
23 months ago paulson 2017-08-23 More tidying, and renaming of theorems
23 months ago paulson 2017-08-23 merged
23 months ago paulson 2017-08-23 More tidying up of monotone_convergence_interval
23 months ago blanchet 2017-08-24 tuning (proofs and code)
23 months ago blanchet 2017-08-24 upgraded CVC4 component to fix abnormal termination reported by Larry Paulson
23 months ago haftmann 2017-08-23 dedicated local for "operative" avoids namespace pollution
23 months ago nipkow 2017-08-23 reorg
23 months ago nipkow 2017-08-23 added lemma
23 months ago eberlm 2017-08-23 Merged
23 months ago Manuel Eberl 2017-08-23 HOL-Library: going_to filter
23 months ago paulson 2017-08-23 more on the dreadful monotone_convergence_interval
23 months ago Manuel Eberl 2017-08-22 Lemmas about analysis and permutations
23 months ago Lars Hupel 2017-08-22 tuned
23 months ago Lars Hupel 2017-08-22 merged
23 months ago Lars Hupel 2017-08-22 tuned syntax
23 months ago wenzelm 2017-08-22 tuned;
23 months ago Lars Hupel 2017-08-22 output syntax for pattern aliases