| Tue, 26 Mar 2013 12:21:01 +0100 | hoelzl | remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces | file | diff | annotate |
| Tue, 26 Mar 2013 12:20:57 +0100 | hoelzl | rename RealVector.thy to Real_Vector_Spaces.thy | file | diff | annotate | base |