src/HOL/NSA/Hyperreal.thy
author hoelzl
Tue Mar 26 12:20:58 2013 +0100 (2013-03-26)
changeset 51525 d3d170a2887f
parent 35310 73806dbabe90
permissions -rw-r--r--
HOL-NSA should only import Complex_Main
haftmann@28952
     1
(*  Title:      HOL/NSA/Hyperreal.thy
huffman@27468
     2
    Author:     Jacques Fleuriot, Cambridge University Computer Laboratory
huffman@27468
     3
    Copyright   1998  University of Cambridge
huffman@27468
     4
huffman@27468
     5
Construction of the Hyperreals by the Ultrapower Construction
huffman@27468
     6
and mechanization of Nonstandard Real Analysis
huffman@27468
     7
*)
huffman@27468
     8
huffman@27468
     9
theory Hyperreal
hoelzl@51525
    10
imports HLog
huffman@27468
    11
begin
huffman@27468
    12
huffman@27468
    13
end