(* Title: HOL/Real/ex/ROOT.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1999 University of Cambridge HOL/Real examples. *) time_use_thy "BinEx";