src/HOL/Library/Topology_Euclidean_Space.thy
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
2009-05-29 huffman 2009-05-29 generalize at function to class perfect_space
2009-05-29 huffman 2009-05-29 generalize topological notions to class metric_space; add class perfect_space
2009-05-29 huffman 2009-05-29 instance ^ :: (metric_space, finite) metric_space
2009-05-29 huffman 2009-05-29 generalize tendsto and related constants to class metric_space
2009-05-29 huffman 2009-05-29 add lemmas Lim_at_iff_LIM, Lim_sequentially_iff_LIMSEQ
2009-05-29 huffman 2009-05-29 remove duplicate cauchy constant
2009-05-28 huffman 2009-05-28 move dist operation to new metric_space class
2009-05-28 huffman 2009-05-28 merged
2009-05-28 huffman 2009-05-28 generalize dist function to class real_normed_vector
2009-05-28 himmelma 2009-05-28 Moved some lemmas about intervals to Topology
2009-05-28 himmelma 2009-05-28 Corrected definition of is_interval
2009-05-28 himmelma 2009-05-28 Changed prioriy of vector_scalar_mult
2009-04-24 haftmann 2009-04-24 removed confusion around funpow
2009-04-20 haftmann 2009-04-20 power operation on functions with syntax o^; power operation on relations with syntax ^^
2009-03-22 haftmann 2009-03-22 merged
2009-03-22 haftmann 2009-03-22 dropped theory Arith_Tools
2009-03-22 nipkow 2009-03-22 1. New cancellation simprocs for common factors in inequations 2. Updated the documentation
2009-03-19 huffman 2009-03-19 imported patch euclidean
2009-03-16 wenzelm 2009-03-16 simplified method setup;