equal
deleted
inserted
replaced
1 (* Title: HOL/Real/ROOT.ML |
1 (* Title: HOL/Real/ROOT.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1998 University of Cambridge |
4 Copyright 1998 University of Cambridge |
5 |
5 |
6 Construction of the Reals using Dedekind Cuts, by Jacques Fleuriot |
6 Construction of the Reals using Dedekind Cuts, Ultrapower Construction |
|
7 of the hyperreals, and mechanization of Nonstandard Real Analysis |
|
8 by Jacques Fleuriot |
7 *) |
9 *) |
8 |
10 |
9 with_path "Hyperreal" use_thy "HyperDef"; |
11 time_use_thy "Real"; |
|
12 with_path "Hyperreal" use_thy "Series"; |
|
13 |
|
14 |
|
15 |