| changeset 61610 | 4f54d2759a0b |
| parent 61609 | 77b453bd616f |
| parent 61560 | 7c985fd653c5 |
| child 61711 | 21d7910d6816 |
--- a/src/HOL/Multivariate_Analysis/Weierstrass.thy Tue Nov 10 14:18:41 2015 +0000 +++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy Tue Nov 10 14:43:29 2015 +0000 @@ -1,8 +1,7 @@ -section\<open>Bernstein-Weierstrass and Stone-Weierstrass Theorems\<close> +section \<open>Bernstein-Weierstrass and Stone-Weierstrass Theorems\<close> theory Weierstrass imports Uniform_Limit Path_Connected - begin (*Power.thy:*)