1
(* Title: HOL/Real/ex/ROOT.ML
2
ID: $Id$
3
4
Miscellaneous HOL-Real Examples.
5
*)
6
7
time_use_thy "BinEx";