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, Ultrapower Construction |
6 Construction of the Reals using Dedekind Cuts |
7 of the hyperreals, and mechanization of Nonstandard Real Analysis |
7 by Jacques Fleuriot |
8 by Jacques Fleuriot |
|
9 *) |
8 *) |
10 |
9 |
11 with_path "Hyperreal" time_use_thy "Hyperreal"; |
10 time_use_thy "Real"; |