src/HOL/Library/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-08-31 nipkow 2009-08-31 tuned the simp rules for Int involving insert and intervals.
2009-08-26 chaieb 2009-08-26 removed unused theorem finite_Atleast_Atmost
2009-06-13 huffman 2009-06-13 generalize lemma connected_real_lemma
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 declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
2009-06-12 huffman 2009-06-12 remove simp add: norm_scaleR
2009-06-11 huffman 2009-06-11 add lemmas about closed sets
2009-06-11 huffman 2009-06-11 new lemmas
2009-06-09 huffman 2009-06-09 merged
2009-06-08 huffman 2009-06-08 lemmas about linear, bilinear
2009-06-09 himmelma 2009-06-09 removed duplicate lemmas
2009-06-07 huffman 2009-06-07 new setL2 lemmas; instance ^ :: (topological_space, finite) topological_space
2009-06-07 huffman 2009-06-07 replace 'topo' with 'open'; add extra type constraint for 'open'
2009-06-04 huffman 2009-06-04 generalize norm method to work over class real_normed_vector
2009-06-03 huffman 2009-06-03 replace class open with class topo
2009-06-03 huffman 2009-06-03 open_dist instance for vectors
2009-06-02 huffman 2009-06-02 instance ^ :: complete_space
2009-06-02 huffman 2009-06-02 generalize lemma norm_pastecart
2009-06-02 huffman 2009-06-02 generalize lemma norm_triangle_sub
2009-06-02 huffman 2009-06-02 new lemmas
2009-05-29 huffman 2009-05-29 instance ^ :: (metric_space, finite) metric_space
2009-05-29 huffman 2009-05-29 fix reference to LIM_def
2009-05-28 huffman 2009-05-28 move dist operation to new metric_space class
2009-05-28 huffman 2009-05-28 generalize dist function to class real_normed_vector
2009-05-28 himmelma 2009-05-28 Changed prioriy of vector_scalar_mult
2009-05-12 chaieb 2009-05-12 Isolated decision procedure for noms and the general arithmetic solver
2009-05-04 haftmann 2009-05-04 dropped duplicate lemma sum_nonneg_eq_zero_iff
2009-04-29 haftmann 2009-04-29 farewell to class recpower
2009-04-22 haftmann 2009-04-22 power operation defined generic
2009-03-23 haftmann 2009-03-23 merged
2009-03-23 haftmann 2009-03-23 tuned header
2009-03-22 haftmann 2009-03-22 tuned header
2009-03-19 huffman 2009-03-19 imported patch euclidean
2009-03-16 wenzelm 2009-03-16 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-12 huffman 2009-03-12 remove trailing spaces
2009-03-05 haftmann 2009-03-05 merged
2009-03-05 haftmann 2009-03-05 tuned
2009-03-04 wenzelm 2009-03-04 removed old/broken CVS Ids;
2009-03-04 chaieb 2009-03-04 fixed proofs; added rules as default simp-rules
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-22 huffman 2009-02-22 remove duplicate instance declaration
2009-02-21 huffman 2009-02-21 real_inner class instance for vectors
2009-02-21 huffman 2009-02-21 remove duplicated lemmas about norm
2009-02-21 huffman 2009-02-21 real_normed_vector instance
2009-02-21 huffman 2009-02-21 fix real_vector, real_algebra instances
2009-02-13 huffman 2009-02-13 section -> subsection
2009-02-13 huffman 2009-02-13 add instance for cancel_comm_monoid_add
2009-02-12 huffman 2009-02-12 fix document generation
2009-02-09 chaieb 2009-02-09 fixed proof -- removed unnecessary sorry
2009-02-09 chaieb 2009-02-09 (Real) Vectors in Euclidean space, and elementary linear algebra.