| author | wenzelm |
| Fri, 14 Dec 2001 11:53:31 +0100 | |
| changeset 12499 | 1b56e1732a61 |
| parent 10751 | a81ea5d3dd41 |
| permissions | -rw-r--r-- |
(* Title: HOL/Hyperreal/ROOT.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge Construction of the Hyperreals by the Ultrapower Construction and mechanization of Nonstandard Real Analysis by Jacques Fleuriot *) time_use_thy "Hyperreal";