src/HOL/Real/ROOT.ML
changeset 10043 a0364652e115
parent 9430 c2dd2780f88d
child 10094 22f201e9ec7a
     1.1 --- a/src/HOL/Real/ROOT.ML	Thu Sep 21 10:42:49 2000 +0200
     1.2 +++ b/src/HOL/Real/ROOT.ML	Thu Sep 21 12:11:38 2000 +0200
     1.3 @@ -3,7 +3,13 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1998  University of Cambridge
     1.6  
     1.7 -Construction of the Reals using Dedekind Cuts, by Jacques Fleuriot
     1.8 +Construction of the Reals using Dedekind Cuts, Ultrapower Construction
     1.9 +of the hyperreals, and mechanization of Nonstandard Real Analysis  
    1.10 +                        by Jacques Fleuriot
    1.11  *)
    1.12  
    1.13 -with_path "Hyperreal" use_thy "HyperDef";
    1.14 +time_use_thy "Real";
    1.15 +with_path "Hyperreal" use_thy "Series";
    1.16 +
    1.17 +
    1.18 +