src/HOL/Analysis/Multivariate_Analysis.thy
Mon, 04 Nov 2019 17:59:32 -0500 immler the division between Starlike and Convex_Euclidean_Space is artificial, therefore include Starlike
Wed, 28 Aug 2019 08:51:20 +0200 immler entry point for analysis without integration theory
less more (0) tip