author | huffman |
Thu, 03 Jul 2008 17:47:22 +0200 | |
changeset 27468 | 0783dd1dc13d |
child 28952 | 15a4b2cf8c34 |
permissions | -rw-r--r-- |
27468 | 1 |
(* Title: HOL/Hyperreal/Hyperreal.thy |
2 |
ID: $Id$ |
|
3 |
Author: Jacques Fleuriot, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Construction of the Hyperreals by the Ultrapower Construction |
|
7 |
and mechanization of Nonstandard Real Analysis |
|
8 |
*) |
|
9 |
||
10 |
theory Hyperreal |
|
11 |
imports Ln Deriv Taylor Integration HLog |
|
12 |
begin |
|
13 |
||
14 |
end |