src/HOL/Import/HOLLight/ROOT.ML

adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening

(*  Title:      HOL/Import/HOLLight/ROOT.ML
    ID:         $Id$
*)

use_thy "HOLLight";