1(*  Title:      HOL/Nonstandard_Analysis/Hyperreal.thy
2    Author:     Jacques Fleuriot, Cambridge University Computer Laboratory
3    Copyright   1998  University of Cambridge
4
5Construction of the Hyperreals by the Ultrapower Construction
6and mechanization of Nonstandard Real Analysis
7*)
8
9theory Hyperreal
10imports HLog
11begin
12
13end
14