(* Title: HOL/Quot/ROOT.ML ID: $Id$ Author: Copyright Higher-order quotients. *) HOL_build_completed; (*Make examples fail if HOL did*) writeln"Root file for HOL/Quot"; (*use_thy "Quot";*)