| Thu, 25 Apr 2013 11:59:21 +0200 | hoelzl | revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space | file | diff | annotate |
| Thu, 25 Apr 2013 10:35:56 +0200 | hoelzl | renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS) | file | diff | annotate |
| 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 |