author | paulson |
Sat, 30 Dec 2000 22:13:18 +0100 | |
changeset 10752 | c4f1bf2acf4c |
parent 10094 | 22f201e9ec7a |
child 12733 | 611ab32b2176 |
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"; |