author | immler |
Mon, 02 Dec 2019 13:41:44 -0500 | |
changeset 71197 | 36961c681fed |
parent 71194 | 26b35a97bddb |
child 71198 | 1bf7d1acbe74 |
--- a/src/HOL/Analysis/Analysis.thy Mon Dec 02 18:29:22 2019 +0100 +++ b/src/HOL/Analysis/Analysis.thy Mon Dec 02 13:41:44 2019 -0500 @@ -6,7 +6,6 @@ (* Topology *) Connected Abstract_Limits - Abstract_Euclidean_Space (* Functional Analysis *) Elementary_Normed_Spaces Norm_Arith @@ -46,6 +45,7 @@ Simplex_Content FPS_Convergence Smooth_Paths + Abstract_Euclidean_Space begin end