| Tue, 09 Apr 2013 14:04:41 +0200 | hoelzl | remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas) | file | diff | annotate |
| 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 |