@Theo, doubtless in the year since you answered this question, someone who can produce such impressive notes would have gotten all the details of a thorough answer sorted out, but my own proof of Lie III from my own forthcoming exposition on Lie theory, for what it's worth, it is basically a turning on its head of the proof that two simply connected connected Lie groups are isomorphic and runs roughly as follows. Once we have the local Lie group, form the set of all formal products of the form $\gamma = \Pi_j \exp\left(X_j(\tau)\right)$ where $X_j(\tau)$ are a $C^1$ paths in the local Lie group, of course small enough that CBH applies to all pairs of its products. Then you can show that all continuous deformations of this path through the set of formal products can be written, thanks to the Hadamard formula, as $\Pi_j \exp\left(X_j(\tau)\right) \Pi_j \exp\left(\delta X_j(\tau)\right)$, i.e. you can shuffle all the variation to one end of the product. Now restrict the variations $\delta X_j$ to be small enough so that the CBH formula applies to each stage of the n-fold product $\Delta = \Pi_j \exp\left(\delta X_j(\tau)\right)$. Thus, even though we have not rigourously defined the "value" of the formal product, now the concept of small continuous, but finite variations of the path that leave the "value" of the formal product unchanged is meaningful - it is any such variation such that, as calculated by CBH, $e = \Delta = \Pi_j \exp\left(\delta X_j(\tau)\right)$ where $e$ is the group identity. So now we can define two of our formal products to be equivalent if one can find a finite sequence of small, continous variations that leave the products "value" unchanged, in the sense defined above, that step-by-step deforms one formal product to the other. We thus condense the big set of formal products into its equivalence classes modulo the equivalence just defined. This approach does two things: $\mathbf{(i)}$ it irons out any inconsitency that might arise from an element's having horribly many potential representations as different formal products and $\mathbf{(ii)}$ the set of equivalence classes, as a set of homotopy classes is simply connected by construction. So now we just check that this beast is a Lie group and we are done: in my exposition this is easy, because I use essentially a converse of Satz 1 of Freudenthal's 1941 "Die Topologie der Lieschen Gruppen Als Algebraisches Phanomen. I" to define a Lie group - I show one can take essentially the properties listed in Freudenthal's theorem, use them as axioms and show that a group that is a simply connected manifold builds itself from them. What we have done, of course, is to build the unique, simply connected connected Lie group that has the Lie algebra "input" to our proof".

I believe my approach is somewhat like the J.P. Serre's 1964 lectures approach cited in the first answer.