isabelle: File revisions

src/HOL/Real_Vector_Spaces.thy

Sat, 15 Jun 2013 17:19:23 +0200	haftmann	pragmatic executability for instance real :: open	file \| diff \| annotate
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

isabelle