Thu, 01 Sep 2011 09:02:14 0700 
huffman 
modernize lemmas about 'continuous' and 'continuous_on';

file 
diff 
annotate

Thu, 25 Aug 2011 19:41:38 0700 
huffman 
replace some continuous_on lemmas with more general versions

file 
diff 
annotate

Tue, 23 Aug 2011 14:11:02 0700 
huffman 
declare euclidean_simps [simp] at the point they are proved;

file 
diff 
annotate

Thu, 18 Aug 2011 13:36:58 0700 
huffman 
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas

file 
diff 
annotate

Wed, 10 Aug 2011 13:13:37 0700 
huffman 
more uniform naming scheme for finite cartesian product type and related theorems

file 
diff 
annotate

Sun, 13 Mar 2011 22:24:10 +0100 
wenzelm 
eliminated hard tabs;

file 
diff 
annotate

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

file 
diff 
annotate

Thu, 01 Jul 2010 15:40:38 0700 
huffman 
convert theorem path_connected_sphere to euclidean_space class

file 
diff 
annotate

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.

file 
diff 
annotate

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

file 
diff 
annotate

Wed, 28 Apr 2010 16:11:07 0700 
huffman 
move pathrelated stuff into new theory file

file 
diff 
annotate

Mon, 26 Apr 2010 15:22:03 0700 
huffman 
move proof of Fashoda meet theorem into separate file

file 
diff 
annotate
