1This chapter provides documentation on all the \ML\ functions that are made
2available in \HOL\ when the \ml{pred\_sets} library is loaded.  This
3documentation is also available online via the \ml{help} facility.
4
5
6