(* Title: HOL/Hyperreal/ex/ROOT.ML ID: $Id$ Miscellaneous HOL-Hyperreal Examples. *) no_document use_thy "Primes"; use_thy "Sqrt"; use_thy "Sqrt_Script";