src/HOL/Real/ROOT.ML
author paulson
Fri, 02 Mar 2007 12:37:34 +0100
changeset 22382 dbf09db0a40d
parent 16828 581764860c2b
permissions -rw-r--r--
New code to store theorem names in a concise form rather than as fully-qualified. Meson.is_fol_term now takes a theory as argument.

(*  Title:      HOL/Real/ROOT.ML
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Construction of the Reals using Dedekind Cuts 
by Jacques Fleuriot
*)

time_use_thy "Float";