author | berghofe |
Fri, 01 Jul 2005 13:54:12 +0200 | |
changeset 16633 | 208ebc9311f2 |
parent 14265 | 95b42e69436c |
child 16782 | b214f21ae396 |
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 |
||
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10094
diff
changeset
|
6 |
Construction of the Reals using Dedekind Cuts |
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10094
diff
changeset
|
7 |
by Jacques Fleuriot |
5078 | 8 |
*) |
9 |
||
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10094
diff
changeset
|
10 |
time_use_thy "Real"; |