Mon, 15 Aug 2011 12:13:46 -0700remove duplicate lemmas eventually_conjI, eventually_and, eventually_false
huffman [Mon, 15 Aug 2011 12:13:46 -0700] rev 45082
remove duplicate lemmas eventually_conjI, eventually_and, eventually_false

Mon, 15 Aug 2011 10:49:48 -0700Topology_Euclidean_Space.thy: organize section headings
huffman [Mon, 15 Aug 2011 10:49:48 -0700] rev 45081
Topology_Euclidean_Space.thy: organize section headings

Mon, 15 Aug 2011 09:08:17 -0700simplify some proofs
huffman [Mon, 15 Aug 2011 09:08:17 -0700] rev 45080
simplify some proofs

Sun, 14 Aug 2011 13:04:57 -0700generalize lemma convergent_subseq_convergent
huffman [Sun, 14 Aug 2011 13:04:57 -0700] rev 45079
generalize lemma convergent_subseq_convergent

Sun, 14 Aug 2011 11:44:12 -0700locale-ize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses
huffman [Sun, 14 Aug 2011 11:44:12 -0700] rev 45078
locale-ize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses

Sun, 14 Aug 2011 10:47:47 -0700locale-ize some constant definitions, so complete_space can inherit from metric_space
huffman [Sun, 14 Aug 2011 10:47:47 -0700] rev 45077
locale-ize some constant definitions, so complete_space can inherit from metric_space

Sun, 14 Aug 2011 10:25:43 -0700generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman [Sun, 14 Aug 2011 10:25:43 -0700] rev 45076
generalize constant 'lim' and limit uniqueness theorems to class t2_space

Tue, 16 Aug 2011 07:17:15 +0900Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Aug 2011 07:17:15 +0900] rev 45075
Quotient Package: make quotient_type work with separate set type

Mon, 15 Aug 2011 22:31:17 +0200updated README;
wenzelm [Mon, 15 Aug 2011 22:31:17 +0200] rev 45074
updated README;

Mon, 15 Aug 2011 21:54:32 +0200touch descendants of edited nodes;
wenzelm [Mon, 15 Aug 2011 21:54:32 +0200] rev 45073
touch descendants of edited nodes;
more precise handling of Graph exceptions;