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