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