src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-21 wenzelm 2014-10-21 merged
2014-10-21 wenzelm 2014-10-21 tuned whitespace;
2014-10-20 hoelzl 2014-10-20 add tendsto_const and tendsto_ident_at as simp and intro rules
2014-09-04 hoelzl 2014-09-04 cleanup Wfrec; introduce dependent_wf/wellorder_choice
2014-08-05 wenzelm 2014-08-05 tuned proofs -- fewer warnings;
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-30 hoelzl 2014-06-30 more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
2014-06-30 hoelzl 2014-06-30 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-06-18 hoelzl 2014-06-18 filters are easier to define with INF on filters.
2014-06-18 hoelzl 2014-06-18 moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
2014-04-26 haftmann 2014-04-26 more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)
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-04-02 hoelzl 2014-04-02 extend continuous_intros; remove continuous_on_intros and isCont_intros
2014-03-26 huffman 2014-03-26 tuned proofs
2014-03-18 immler 2014-03-18 removed dependencies on theory Ordered_Euclidean_Space
2014-03-18 immler 2014-03-18 use cbox to relax class constraints
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2014-03-13 nipkow 2014-03-13 enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
2014-03-05 huffman 2014-03-05 generalize lemmas
2014-02-27 paulson 2014-02-27 A bit of tidying up
2014-02-16 wenzelm 2014-02-16 tuned proofs;
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2013-12-18 hoelzl 2013-12-18 modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
2013-12-16 immler 2013-12-16 summarized notions related to ordered_euclidean_space and intervals in separate theory
2013-12-16 immler 2013-12-16 prefer box over greaterThanLessThan on euclidean_space
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-05 hoelzl 2013-11-05 move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
2013-11-05 hoelzl 2013-11-05 use INF and SUP on conditionally complete lattices in multivariate analysis
2013-11-05 hoelzl 2013-11-05 add SUP and INF for conditionally complete lattices
2013-11-05 hoelzl 2013-11-05 use bdd_above and bdd_below for conditionally complete lattices
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-10-07 huffman 2013-10-07 new topological lemmas; tuned proofs
2013-09-24 huffman 2013-09-24 generalize lemma
2013-09-24 huffman 2013-09-24 removed unused lemma
2013-09-24 huffman 2013-09-24 factor out new lemma
2013-09-24 huffman 2013-09-24 replace lemma with more general simp rule
2013-09-23 huffman 2013-09-23 tuned proofs
2013-09-14 wenzelm 2013-09-14 tuned proofs;
2013-09-12 huffman 2013-09-12 remove duplicate lemmas
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-29 wenzelm 2013-08-29 tuned proofs;
2013-08-29 wenzelm 2013-08-29 tuned proofs;
2013-08-29 wenzelm 2013-08-29 tuned proofs;
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-07-12 wenzelm 2013-07-12 tuned;
2013-07-12 wenzelm 2013-07-12 tuned proofs;
2013-05-25 haftmann 2013-05-25 weaker precendence of syntax for big intersection and union on sets
2013-04-24 hoelzl 2013-04-24 spell conditional_ly_-complete lattices correct
2013-04-09 hoelzl 2013-04-09 remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
2013-03-26 hoelzl 2013-03-26 rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
2013-03-26 hoelzl 2013-03-26 separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
2013-03-22 hoelzl 2013-03-22 move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
2013-03-22 hoelzl 2013-03-22 move connected to HOL image; used to show intermediate value theorem
2013-03-22 hoelzl 2013-03-22 move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets