Wed, 03 Jun 2009 10:02:59 -0700 | huffman | generalize some constants and lemmas to class topological_space | changeset | files |
Wed, 03 Jun 2009 09:58:11 -0700 | huffman | replace class open with class topo | changeset | files |
Wed, 03 Jun 2009 08:46:13 -0700 | huffman | open_dist instance for vectors | changeset | files |
Wed, 03 Jun 2009 08:43:29 -0700 | huffman | instance * :: topological_space | changeset | files |
Wed, 03 Jun 2009 08:43:01 -0700 | huffman | class real_inner derives from open_dist | changeset | files |
Wed, 03 Jun 2009 07:44:56 -0700 | huffman | introduce class topological_space as a superclass of metric_space | changeset | files |