src/HOL/Analysis/Weierstrass_Theorems.thy
changeset 69517 dc20f278e8f3
parent 69508 2a4c8a2a3f8e
child 69597 ff784d5a5bfb
equal deleted inserted replaced
69516:09bb8f470959 69517:dc20f278e8f3
     1 section \<open>The Bernstein-Weierstrass and Stone-Weierstrass Theorems\<close>
     1 section \<open>Bernstein-Weierstrass and Stone-Weierstrass\<close>
     2 
     2 
     3 text\<open>By L C Paulson (2015)\<close>
     3 text\<open>By L C Paulson (2015)\<close>
     4 
     4 
     5 theory Weierstrass_Theorems
     5 theory Weierstrass_Theorems
     6 imports Uniform_Limit Path_Connected Derivative
     6 imports Uniform_Limit Path_Connected Derivative