src/HOL/Real/ROOT.ML
author fleuriot
Thu Sep 21 12:11:38 2000 +0200 (2000-09-21)
changeset 10043 a0364652e115
parent 9430 c2dd2780f88d
child 10094 22f201e9ec7a
permissions -rw-r--r--
Updated Files with new theorems
     1 (*  Title:      HOL/Real/ROOT.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Construction of the Reals using Dedekind Cuts, Ultrapower Construction
     7 of the hyperreals, and mechanization of Nonstandard Real Analysis  
     8                         by Jacques Fleuriot
     9 *)
    10 
    11 time_use_thy "Real";
    12 with_path "Hyperreal" use_thy "Series";
    13 
    14 
    15