1
(* Title: HOL/Quot/ROOT.ML
2
ID: $Id$
3
Author:
4
Copyright
5
6
Higher-order quotients.
7
*)
8
9
HOL_build_completed; (*Make examples fail if HOL did*)
10
11
writeln"Root file for HOL/Quot";
12
13
use_thy "FRACT";
14