src/HOL/Multivariate_Analysis/Fashoda.thy
2014-03-18 immler 2014-03-18 use cbox to relax class constraints
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2014-02-22 wenzelm 2014-02-22 tuned proofs;
2013-12-16 immler 2013-12-16 prefer box over greaterThanLessThan on euclidean_space
2013-09-13 wenzelm 2013-09-13 tuned proofs;
2013-09-13 wenzelm 2013-09-13 tuned proofs;
2013-09-11 wenzelm 2013-09-11 tuned proofs;
2013-03-22 hoelzl 2013-03-22 introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
2012-12-14 hoelzl 2012-12-14 Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
2011-09-01 huffman 2011-09-01 modernize lemmas about 'continuous' and 'continuous_on'; improve automation of continuity proofs;
2011-08-25 huffman 2011-08-25 replace some continuous_on lemmas with more general versions
2011-08-23 huffman 2011-08-23 declare euclidean_simps [simp] at the point they are proved; avoid duplicate rule warnings;
2011-08-18 huffman 2011-08-18 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-08-10 huffman 2011-08-10 more uniform naming scheme for finite cartesian product type and related theorems
2011-03-13 wenzelm 2011-03-13 eliminated hard tabs;
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-07-01 huffman 2010-07-01 convert theorem path_connected_sphere to euclidean_space class
2010-06-21 hoelzl 2010-06-21 Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
2010-04-29 huffman 2010-04-29 define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
2010-04-28 huffman 2010-04-28 move path-related stuff into new theory file
2010-04-26 huffman 2010-04-26 move proof of Fashoda meet theorem into separate file