src/HOL/NSA/Hyperreal.thy
author hoelzl
Tue Feb 23 12:02:32 2010 +0100 (2010-02-23)
changeset 35310 73806dbabe90
parent 28952 15a4b2cf8c34
child 51525 d3d170a2887f
permissions -rw-r--r--
Forgot to check NSA in changeset e4a431b6d9b7 ; Removed import of Integration
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@35310
    10
imports Ln Deriv Taylor HLog
huffman@27468
    11
begin
huffman@27468
    12
huffman@27468
    13
end