isabelle: src/HOL/Hyperreal/ROOT.ML@27e4d90b35b5 (annotated)

10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	1	(* Title: HOL/Hyperreal/ROOT.ML
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	2	ID: $Id$
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	4	Copyright 1998 University of Cambridge
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	5
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	6	Construction of the Hyperreals by the Ultrapower Construction
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	7	and mechanization of Nonstandard Real Analysis
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	8	by Jacques Fleuriot
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	9	*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	10
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	11	time_use_thy "Hyperreal";