src/HOL/Real/ROOT.ML
changeset 10094 22f201e9ec7a
parent 10043 a0364652e115
child 10752 c4f1bf2acf4c
     1.1 --- a/src/HOL/Real/ROOT.ML	Wed Sep 27 19:34:46 2000 +0200
     1.2 +++ b/src/HOL/Real/ROOT.ML	Wed Sep 27 19:36:31 2000 +0200
     1.3 @@ -4,12 +4,8 @@
     1.4      Copyright   1998  University of Cambridge
     1.5  
     1.6  Construction of the Reals using Dedekind Cuts, Ultrapower Construction
     1.7 -of the hyperreals, and mechanization of Nonstandard Real Analysis  
     1.8 +of the hyperreals, and mechanization of Nonstandard Real Analysis
     1.9                          by Jacques Fleuriot
    1.10  *)
    1.11  
    1.12 -time_use_thy "Real";
    1.13 -with_path "Hyperreal" use_thy "Series";
    1.14 -
    1.15 -
    1.16 -
    1.17 +with_path "Hyperreal" time_use_thy "Hyperreal";