Loeb Measure construction in axiomatic approach to NSA Hello dear StackExchange,
in my upcoming bachelor's thesis, I plan to present an overview of some topics in nonstandard analysis, including some higher applications, like Loeb Measures (among other things). This turns out to be more confusing to realise than I hoped.
Now since this is just a bachelor's thesis, space is limited and 40 - 50 pages would already be rather long. Therefore, constructing the hyperreals from scratch via the ultrapower construction and then developing Loeb Measures is simply too much. 
(although I'm not opposed to working through this to gain a deeper understanding of the topics at hand; fortunately, I learned the necessary background knowledge in my logic course)
Naturally, the next best option is an axiomatic approach, which is generally a good choice since my professor is probably more interested in direct application of NSA rather than all the machinery behind it.
Fortunately, there are already several axiomatic treatments of NSA, presenting conservative extensions of ZFC, for example Nelson's internal set theory and Hrbaceks external set theories - but regarding the construction of Loeb Measures, I have only found resources using the ultrapower construction beforehand.
So finally, my question is if there are any resources (if it's possible) where the axiomatic approach is used to shortcut all the logic and set theory, so that mathematicians unschooled in those topics can apply NSA methods to (for example) probability, using Loeb Measures.
Also, I am a bit overwhelmed by the number of different approaches with different pros and cons, and which one to choose, so any help is appreciated.
Thanks in advance!
 A: Goldblatt's text is accessible to undergraduates with some exposure to analysis. The ultrapower construction of the hyperreals there is some brief ten pages (with commentary), after which the chapter on Los's theorem should be reviewed for its implications for hyperreals. There is a section on Loeb measures as well in Goldblatt which may or may not be useful for your purposes.
The ultrapower construction is not so technical. It can be worked through quickly once one is familiar with the concept of an ultrafilter.
A: In the paper Approaches to analysis with infinitesimals following Robinson, Nelson and others, you can find a (long) survey of approaches to nonstandard analysis.
At page 13 there is possibly the shortest definition of Loeb measure over [0,1]. Of course, all the proofs of the properties of the Loeb measure and many more details are omitted from this presentation.
Section 5 contains a presentation of some axiomatic approaches to NSA; however, these are far from being elementary.
There are also two lesser-known axiomatic approaches by Benci and Di Nasso, namely alpha- and lambda-theory presented for instance in Section 1 of Alpha-theory: an elementary axiomatics for nonstandard analysis and in Section 2 of Ultrafunctions and Generalized Solutions. However you will not find the construction of the Loeb measure in any of these papers.
Another classic reference is Loeb Measures in Practice: Recent Advances by Cutland.
