| Tue, 09 Apr 2013 14:04:47 +0200 | hoelzl | move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative | file | diff | annotate |
| 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 |