author | nipkow |
Thu, 12 Oct 2000 18:38:23 +0200 | |
changeset 10212 | 33fe2d701ddd |
parent 10094 | 22f201e9ec7a |
child 10752 | c4f1bf2acf4c |
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 |
10094 | 7 |
of the hyperreals, and mechanization of Nonstandard Real Analysis |
10043 | 8 |
by Jacques Fleuriot |
5078 | 9 |
*) |
10 |
||
10094 | 11 |
with_path "Hyperreal" time_use_thy "Hyperreal"; |