| changeset 69517 | dc20f278e8f3 |
| parent 69508 | 2a4c8a2a3f8e |
| child 69597 | ff784d5a5bfb |
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy Thu Dec 27 23:38:55 2018 +0100 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Fri Dec 28 10:29:59 2018 +0100 @@ -1,4 +1,4 @@ -section \<open>The Bernstein-Weierstrass and Stone-Weierstrass Theorems\<close> +section \<open>Bernstein-Weierstrass and Stone-Weierstrass\<close> text\<open>By L C Paulson (2015)\<close>