src/HOL/Hyperreal/ROOT.ML

+(*  Title:      HOL/Hyperreal/ROOT.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Construction of the Hyperreals by the Ultrapower Construction
+and mechanization of Nonstandard Real Analysis
+by Jacques Fleuriot
+*)
+
+time_use_thy "Hyperreal";