author | fleuriot |
Thu, 21 Sep 2000 12:11:38 +0200 | |
changeset 10043 | a0364652e115 |
parent 9430 | c2dd2780f88d |
child 10094 | 22f201e9ec7a |
permissions | -rw-r--r-- |
9108 | 1 |
(* Title: HOL/Real/ROOT.ML |
5078 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
10043 | 6 |
Construction of the Reals using Dedekind Cuts, Ultrapower Construction |
7 |
of the hyperreals, and mechanization of Nonstandard Real Analysis |
|
8 |
by Jacques Fleuriot |
|
5078 | 9 |
*) |
10 |
||
10043 | 11 |
time_use_thy "Real"; |
12 |
with_path "Hyperreal" use_thy "Series"; |
|
13 |
||
14 |
||
15 |