src/HOL/Multivariate_Analysis/Fashoda.thy
Wed, 10 Jun 2015 19:10:20 +0200 wenzelm isabelle update_cartouches;
Wed, 18 Feb 2015 22:46:48 +0100 haftmann eliminated fact duplicates
Sun, 02 Nov 2014 17:09:04 +0100 wenzelm modernized header;
Sun, 21 Sep 2014 16:56:11 +0200 haftmann explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
Sat, 28 Jun 2014 09:16:42 +0200 haftmann fact consolidation
Mon, 14 Apr 2014 13:08:17 +0200 hoelzl added divide_nonneg_nonneg and co; made it a simp rule
Wed, 02 Apr 2014 18:35:07 +0200 hoelzl extend continuous_intros; remove continuous_on_intros and isCont_intros
Tue, 25 Mar 2014 14:20:58 +0100 hoelzl cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
Tue, 18 Mar 2014 10:12:58 +0100 immler removed dependencies on theory Ordered_Euclidean_Space
Tue, 18 Mar 2014 10:12:57 +0100 immler use cbox to relax class constraints
Sat, 15 Mar 2014 08:31:33 +0100 haftmann more complete set of lemmas wrt. image and composition
Sat, 22 Feb 2014 22:06:10 +0100 wenzelm tuned proofs;
Mon, 16 Dec 2013 17:08:22 +0100 immler prefer box over greaterThanLessThan on euclidean_space
Fri, 13 Sep 2013 22:31:56 +0200 wenzelm tuned proofs;
Fri, 13 Sep 2013 22:16:26 +0200 wenzelm tuned proofs;
Wed, 11 Sep 2013 20:34:45 +0200 wenzelm tuned proofs;
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
Fri, 14 Dec 2012 15:46:01 +0100 hoelzl Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
Thu, 01 Sep 2011 09:02:14 -0700 huffman modernize lemmas about 'continuous' and 'continuous_on';
Thu, 25 Aug 2011 19:41:38 -0700 huffman replace some continuous_on lemmas with more general versions
Tue, 23 Aug 2011 14:11:02 -0700 huffman declare euclidean_simps [simp] at the point they are proved;
Thu, 18 Aug 2011 13:36:58 -0700 huffman remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
Wed, 10 Aug 2011 13:13:37 -0700 huffman more uniform naming scheme for finite cartesian product type and related theorems
Sun, 13 Mar 2011 22:24:10 +0100 wenzelm eliminated hard tabs;
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Thu, 01 Jul 2010 15:40:38 -0700 huffman convert theorem path_connected_sphere to euclidean_space class
Mon, 21 Jun 2010 19:33:51 +0200 hoelzl Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
Thu, 29 Apr 2010 11:41:04 -0700 huffman 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
Wed, 28 Apr 2010 16:11:07 -0700 huffman move path-related stuff into new theory file
Mon, 26 Apr 2010 15:22:03 -0700 huffman move proof of Fashoda meet theorem into separate file
less more (0) tip