equal
deleted
inserted
replaced
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, by Jacques Fleuriot |
7 |
|
8 Linear real arithmetic is installed in RealBin.ML. |
|
9 *) |
7 *) |
10 |
8 |
11 with_path "Hyperreal" use_thy "HyperDef"; |
9 with_path "Hyperreal" use_thy "HyperDef"; |