src/HOL/Library/Topology_Euclidean_Space.thy
2009-10-27 paulson 2009-10-27 New theory SupInf of the supremum and infimum operators for sets of reals.
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-23 haftmann 2009-09-23 inf/sup_absorb are no default simp rules any longer
2009-09-21 haftmann 2009-09-21 tuned proofs
2009-06-25 haftmann 2009-06-25 arbitrary farewell
2009-06-13 huffman 2009-06-13 generalize lemmas
2009-06-13 huffman 2009-06-13 replace uses of (bi)linear with bounded_(bi)linear
2009-06-13 huffman 2009-06-13 new continuous/vimage lemmas; cleaned up proofs
2009-06-13 huffman 2009-06-13 generalize constants netlimit and continuous
2009-06-13 huffman 2009-06-13 generalize lemma Lim_unique to t2_space
2009-06-12 huffman 2009-06-12 generalize lemmas about inner
2009-06-12 huffman 2009-06-12 replace all occurrences of dot at type real^'n with inner
2009-06-12 huffman 2009-06-12 avoid using vec1 in continuity lemmas
2009-06-12 huffman 2009-06-12 remove simp add: norm_scaleR
2009-06-12 huffman 2009-06-12 replace all occurrences of 'op *s' at type real^'n with scaleR
2009-06-11 huffman 2009-06-11 move lemma compact_Times; generalize more lemmas
2009-06-11 huffman 2009-06-11 generalize lemma edelstein_fix
2009-06-11 huffman 2009-06-11 generalize lemmas
2009-06-11 huffman 2009-06-11 theorem attribute [tendsto_intros]
2009-06-10 huffman 2009-06-10 heine_borel instance for products
2009-06-10 huffman 2009-06-10 use constants subseq, incseq, monoseq
2009-06-09 huffman 2009-06-09 remove uses of vec1 in continuity lemmas
2009-06-09 huffman 2009-06-09 instance heine_borel < complete_space; generalize many lemmas to class heine_borel
2009-06-09 huffman 2009-06-09 new class heine_borel for lemma bounded_closed_imp_compact; instances for real, ^
2009-06-08 huffman 2009-06-08 generalize compact/closure lemmas
2009-06-08 huffman 2009-06-08 add lemma complete_imp_closed
2009-06-08 huffman 2009-06-08 generalize constant 'bounded' to class metric_space
2009-06-08 huffman 2009-06-08 generalize lemmas compact_imp_bounded, compact_imp_closed
2009-06-08 huffman 2009-06-08 generalize more lemmas
2009-06-08 huffman 2009-06-08 generalize constant 'indirection'
2009-06-08 huffman 2009-06-08 lemmas about linear, bilinear
2009-06-08 huffman 2009-06-08 generalize constant 'complete'
2009-06-08 huffman 2009-06-08 generalize lemmas eventually_within_interior, lim_within_interior
2009-06-08 huffman 2009-06-08 generalize more lemmas
2009-06-08 huffman 2009-06-08 generalize some lemmas
2009-06-07 huffman 2009-06-07 replace 'topo' with 'open'; add extra type constraint for 'open'
2009-06-07 huffman 2009-06-07 move definitions of open, closed to RealVector.thy
2009-06-06 huffman 2009-06-06 lemmas islimptI, islimptE; generalize open_inter_closure_subset
2009-06-06 huffman 2009-06-06 generalize tendsto to class topological_space
2009-06-05 huffman 2009-06-05 put syntax for tendsto in Limits.thy; rename variables
2009-06-05 haftmann 2009-06-05 merged
2009-06-04 haftmann 2009-06-04 class replaces axclass
2009-06-04 huffman 2009-06-04 define netlimit in terms of eventually
2009-06-04 huffman 2009-06-04 generalize type of 'at' to topological_space; generalize some lemmas
2009-06-04 huffman 2009-06-04 generalize norm method to work over class real_normed_vector
2009-06-03 huffman 2009-06-03 add classes for t0, t1, and t2 spaces
2009-06-03 huffman 2009-06-03 generalize type of islimpt
2009-06-03 huffman 2009-06-03 generalize some constants and lemmas to class topological_space
2009-06-02 huffman 2009-06-02 generalize constant uniformly_continuous_on
2009-06-02 huffman 2009-06-02 generalize more constants
2009-06-02 huffman 2009-06-02 generalize type of bounded
2009-06-02 huffman 2009-06-02 generalize lemma Lim_unique
2009-06-02 huffman 2009-06-02 generalize lemma closed_cball
2009-06-02 huffman 2009-06-02 generalize Lim_transform lemmas
2009-06-02 huffman 2009-06-02 generalize lemma interior_closed_Un_empty_interior
2009-06-02 huffman 2009-06-02 reuse definition of nets from Limits.thy
2009-06-02 huffman 2009-06-02 generalize type of 'at' to metric_space
2009-06-02 huffman 2009-06-02 redefine nets as filter bases
2009-05-31 huffman 2009-05-31 more abstract properties of eventually
2009-05-31 huffman 2009-05-31 new lemmas about eventually; rewrite Lim proofs to use more abstract properties of eventually