src/HOL/Real/ex/ROOT.ML

Goal: tuned pris;

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

HOL/Real examples.
*)

writeln "Root file for HOL/Real examples";

set proof_timing;

time_use_thy "BinEx";