src/HOL/Analysis/Weierstrass_Theorems.thy
changeset 63940 0d82c4c94014
parent 63938 f6ce08859d4c
child 64267 b9a1486e79be