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
wenzelm@9108
     1
(*  Title:      HOL/Real/ROOT.ML
paulson@5078
     2
    ID:         $Id$
paulson@5078
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5078
     4
    Copyright   1998  University of Cambridge
paulson@5078
     5
fleuriot@10043
     6
Construction of the Reals using Dedekind Cuts, Ultrapower Construction
fleuriot@10043
     7
of the hyperreals, and mechanization of Nonstandard Real Analysis  
fleuriot@10043
     8
                        by Jacques Fleuriot
paulson@5078
     9
*)
paulson@5078
    10
fleuriot@10043
    11
time_use_thy "Real";
fleuriot@10043
    12
with_path "Hyperreal" use_thy "Series";
fleuriot@10043
    13
fleuriot@10043
    14
fleuriot@10043
    15