----------------------------------------------------------------------

Committing in revised source files for building the predicate set
library documentation.

Doing "make all" in the hol98/src/pred_set/Manual directory should
create .dvi, .ps, and .pdf versions, including the chapter 3 on
preproven theorems and the 4-page index at the end.

If anyone has problems building this, please let me know.

Peter

Modified Files:
hol98/Manual/Quick/quick.tex
hol98/src/pred_set/Manual/Makefile
hol98/src/pred_set/Manual/index.tex
hol98/src/pred_set/Manual/pred_sets.tex
Added Files:
hol98/src/pred_set/help/thms/card/CARD_DEF.doc
hol98/src/pred_set/help/thms/card/CARD_DELETE.doc
hol98/src/pred_set/help/thms/card/CARD_DIFF.doc
hol98/src/pred_set/help/thms/card/CARD_EMPTY.doc
hol98/src/pred_set/help/thms/card/CARD_EQ_0.doc
hol98/src/pred_set/help/thms/card/CARD_INSERT.doc
hol98/src/pred_set/help/thms/card/CARD_INTER_LESS_EQ.doc
hol98/src/pred_set/help/thms/card/CARD_PSUBSET.doc
hol98/src/pred_set/help/thms/card/CARD_SING.doc
hol98/src/pred_set/help/thms/card/CARD_SUBSET.doc
hol98/src/pred_set/help/thms/card/CARD_UNION.doc
hol98/src/pred_set/help/thms/card/LESS_CARD_DIFF.doc
hol98/src/pred_set/help/thms/card/SING_IFF_CARD1.doc
hol98/src/pred_set/help/thms/chre/CHOICE_DEF.doc
hol98/src/pred_set/help/thms/chre/CHOICE_INSERT_REST.doc
hol98/src/pred_set/help/thms/chre/CHOICE_NOT_IN_REST.doc
hol98/src/pred_set/help/thms/chre/CHOICE_SING.doc
hol98/src/pred_set/help/thms/chre/REST_DEF.doc
hol98/src/pred_set/help/thms/chre/REST_PSUBSET.doc
hol98/src/pred_set/help/thms/chre/REST_SING.doc
hol98/src/pred_set/help/thms/chre/REST_SUBSET.doc
hol98/src/pred_set/help/thms/chre/SING_IFF_EMPTY_REST.doc
hol98/src/pred_set/help/thms/diff/DIFF_DEF.doc
hol98/src/pred_set/help/thms/diff/DIFF_DIFF.doc
hol98/src/pred_set/help/thms/diff/DIFF_EMPTY.doc
hol98/src/pred_set/help/thms/diff/DIFF_EQ_EMPTY.doc
hol98/src/pred_set/help/thms/diff/DIFF_UNIV.doc
hol98/src/pred_set/help/thms/diff/EMPTY_DIFF.doc
hol98/src/pred_set/help/thms/diff/IN_DIFF.doc
hol98/src/pred_set/help/thms/disj/DISJOINT_DEF.doc
hol98/src/pred_set/help/thms/disj/DISJOINT_DELETE_SYM.doc
hol98/src/pred_set/help/thms/disj/DISJOINT_EMPTY.doc
hol98/src/pred_set/help/thms/disj/DISJOINT_EMPTY_REFL.doc
hol98/src/pred_set/help/thms/disj/DISJOINT_SYM.doc
hol98/src/pred_set/help/thms/disj/DISJOINT_UNION.doc
hol98/src/pred_set/help/thms/disj/IN_DISJOINT.doc
hol98/src/pred_set/help/thms/emuniv/EMPTY_DEF.doc
hol98/src/pred_set/help/thms/emuniv/EMPTY_NOT_UNIV.doc
hol98/src/pred_set/help/thms/emuniv/EQ_UNIV.doc
hol98/src/pred_set/help/thms/emuniv/IN_UNIV.doc
hol98/src/pred_set/help/thms/emuniv/MEMBER_NOT_EMPTY.doc
hol98/src/pred_set/help/thms/emuniv/NOT_IN_EMPTY.doc
hol98/src/pred_set/help/thms/emuniv/UNIV_DEF.doc
hol98/src/pred_set/help/thms/emuniv/UNIV_NOT_EMPTY.doc
hol98/src/pred_set/help/thms/fin/FINITE_DEF.doc
hol98/src/pred_set/help/thms/fin/FINITE_DELETE.doc
hol98/src/pred_set/help/thms/fin/FINITE_DIFF.doc
hol98/src/pred_set/help/thms/fin/FINITE_EMPTY.doc
hol98/src/pred_set/help/thms/fin/FINITE_INDUCT.doc
hol98/src/pred_set/help/thms/fin/FINITE_INSERT.doc
hol98/src/pred_set/help/thms/fin/FINITE_ISO_NUM.doc
hol98/src/pred_set/help/thms/fin/FINITE_PSUBSET_INFINITE.doc
hol98/src/pred_set/help/thms/fin/FINITE_PSUBSET_UNIV.doc
hol98/src/pred_set/help/thms/fin/FINITE_UNION.doc
hol98/src/pred_set/help/thms/fin/IMAGE_11_INFINITE.doc
hol98/src/pred_set/help/thms/fin/IMAGE_FINITE.doc
hol98/src/pred_set/help/thms/fin/INFINITE_DEF.doc
hol98/src/pred_set/help/thms/fin/INFINITE_DIFF_FINITE.doc
hol98/src/pred_set/help/thms/fin/INFINITE_SUBSET.doc
hol98/src/pred_set/help/thms/fin/INFINITE_UNIV.doc
hol98/src/pred_set/help/thms/fin/INTER_FINITE.doc
hol98/src/pred_set/help/thms/fin/IN_INFINITE_NOT_FINITE.doc
hol98/src/pred_set/help/thms/fin/NOT_IN_FINITE.doc
hol98/src/pred_set/help/thms/fin/PSUBSET_FINITE.doc
hol98/src/pred_set/help/thms/fin/SUBSET_FINITE.doc
hol98/src/pred_set/help/thms/fun/BIJ_COMPOSE.doc
hol98/src/pred_set/help/thms/fun/BIJ_DEF.doc
hol98/src/pred_set/help/thms/fun/BIJ_EMPTY.doc
hol98/src/pred_set/help/thms/fun/BIJ_ID.doc
hol98/src/pred_set/help/thms/fun/IMAGE_SURJ.doc
hol98/src/pred_set/help/thms/fun/INJ_COMPOSE.doc
hol98/src/pred_set/help/thms/fun/INJ_DEF.doc
hol98/src/pred_set/help/thms/fun/INJ_EMPTY.doc
hol98/src/pred_set/help/thms/fun/INJ_ID.doc
hol98/src/pred_set/help/thms/fun/LINV_DEF.doc
hol98/src/pred_set/help/thms/fun/RINV_DEF.doc
hol98/src/pred_set/help/thms/fun/SURJ_COMPOSE.doc
hol98/src/pred_set/help/thms/fun/SURJ_DEF.doc
hol98/src/pred_set/help/thms/fun/SURJ_EMPTY.doc
hol98/src/pred_set/help/thms/fun/SURJ_ID.doc
hol98/src/pred_set/help/thms/image/IMAGE_COMPOSE.doc
hol98/src/pred_set/help/thms/image/IMAGE_DEF.doc
hol98/src/pred_set/help/thms/image/IMAGE_DELETE.doc
hol98/src/pred_set/help/thms/image/IMAGE_EMPTY.doc
hol98/src/pred_set/help/thms/image/IMAGE_EQ_EMPTY.doc
hol98/src/pred_set/help/thms/image/IMAGE_ID.doc
hol98/src/pred_set/help/thms/image/IMAGE_IN.doc
hol98/src/pred_set/help/thms/image/IMAGE_INSERT.doc
hol98/src/pred_set/help/thms/image/IMAGE_INTER.doc
hol98/src/pred_set/help/thms/image/IMAGE_SUBSET.doc
hol98/src/pred_set/help/thms/image/IMAGE_UNION.doc
hol98/src/pred_set/help/thms/image/IN_IMAGE.doc
hol98/src/pred_set/help/thms/insdel/ABSORPTION.doc
hol98/src/pred_set/help/thms/insdel/COMPONENT.doc
hol98/src/pred_set/help/thms/insdel/DECOMPOSITION.doc
hol98/src/pred_set/help/thms/insdel/DELETE_COMM.doc
hol98/src/pred_set/help/thms/insdel/DELETE_DEF.doc
hol98/src/pred_set/help/thms/insdel/DELETE_DELETE.doc
hol98/src/pred_set/help/thms/insdel/DELETE_INSERT.doc
hol98/src/pred_set/help/thms/insdel/DELETE_NON_ELEMENT.doc
hol98/src/pred_set/help/thms/insdel/DELETE_SUBSET.doc
hol98/src/pred_set/help/thms/insdel/DIFF_INSERT.doc
hol98/src/pred_set/help/thms/insdel/DISJOINT_INSERT.doc
hol98/src/pred_set/help/thms/insdel/EMPTY_DELETE.doc
hol98/src/pred_set/help/thms/insdel/INSERT_COMM.doc
hol98/src/pred_set/help/thms/insdel/INSERT_DEF.doc
hol98/src/pred_set/help/thms/insdel/INSERT_DELETE.doc
hol98/src/pred_set/help/thms/insdel/INSERT_DIFF.doc
hol98/src/pred_set/help/thms/insdel/INSERT_INSERT.doc
hol98/src/pred_set/help/thms/insdel/INSERT_INTER.doc
hol98/src/pred_set/help/thms/insdel/INSERT_SUBSET.doc
hol98/src/pred_set/help/thms/insdel/INSERT_UNION.doc
hol98/src/pred_set/help/thms/insdel/INSERT_UNION_EQ.doc
hol98/src/pred_set/help/thms/insdel/INSERT_UNIV.doc
hol98/src/pred_set/help/thms/insdel/IN_DELETE.doc
hol98/src/pred_set/help/thms/insdel/IN_DELETE_EQ.doc
hol98/src/pred_set/help/thms/insdel/IN_INSERT.doc
hol98/src/pred_set/help/thms/insdel/NOT_EMPTY_INSERT.doc
hol98/src/pred_set/help/thms/insdel/NOT_INSERT_EMPTY.doc
hol98/src/pred_set/help/thms/insdel/PSUBSET_INSERT_SUBSET.doc
hol98/src/pred_set/help/thms/insdel/SET_CASES.doc
hol98/src/pred_set/help/thms/insdel/SUBSET_DELETE.doc
hol98/src/pred_set/help/thms/insdel/SUBSET_INSERT.doc
hol98/src/pred_set/help/thms/insdel/SUBSET_INSERT_DELETE.doc
hol98/src/pred_set/help/thms/mem/EXTENSION.doc
hol98/src/pred_set/help/thms/mem/GSPECIFICATION.doc
hol98/src/pred_set/help/thms/mem/NOT_EQUAL_SETS.doc
hol98/src/pred_set/help/thms/mem/NUM_SET_WOP.doc
hol98/src/pred_set/help/thms/mem/SET_MINIMUM.doc
hol98/src/pred_set/help/thms/mem/SPECIFICATION.doc
hol98/src/pred_set/help/thms/sing/DELETE_EQ_SING.doc
hol98/src/pred_set/help/thms/sing/DISJOINT_SING_EMPTY.doc
hol98/src/pred_set/help/thms/sing/EQUAL_SING.doc
hol98/src/pred_set/help/thms/sing/FINITE_SING.doc
hol98/src/pred_set/help/thms/sing/INSERT_SING_UNION.doc
hol98/src/pred_set/help/thms/sing/IN_SING.doc
hol98/src/pred_set/help/thms/sing/NOT_EMPTY_SING.doc
hol98/src/pred_set/help/thms/sing/NOT_SING_EMPTY.doc
hol98/src/pred_set/help/thms/sing/SING.doc
hol98/src/pred_set/help/thms/sing/SING_DEF.doc
hol98/src/pred_set/help/thms/sing/SING_DELETE.doc
hol98/src/pred_set/help/thms/sing/SING_FINITE.doc
hol98/src/pred_set/help/thms/subs/EMPTY_SUBSET.doc
hol98/src/pred_set/help/thms/subs/NOT_PSUBSET_EMPTY.doc
hol98/src/pred_set/help/thms/subs/NOT_UNIV_PSUBSET.doc
hol98/src/pred_set/help/thms/subs/PSUBSET_DEF.doc
hol98/src/pred_set/help/thms/subs/PSUBSET_IRREFL.doc
hol98/src/pred_set/help/thms/subs/PSUBSET_MEMBER.doc
hol98/src/pred_set/help/thms/subs/PSUBSET_TRANS.doc
hol98/src/pred_set/help/thms/subs/PSUBSET_UNIV.doc
hol98/src/pred_set/help/thms/subs/SUBSET_ANTISYM.doc
hol98/src/pred_set/help/thms/subs/SUBSET_DEF.doc
hol98/src/pred_set/help/thms/subs/SUBSET_EMPTY.doc
hol98/src/pred_set/help/thms/subs/SUBSET_REFL.doc
hol98/src/pred_set/help/thms/subs/SUBSET_TRANS.doc
hol98/src/pred_set/help/thms/subs/SUBSET_UNIV.doc
hol98/src/pred_set/help/thms/subs/UNIV_SUBSET.doc
hol98/src/pred_set/help/thms/unin/DELETE_INTER.doc
hol98/src/pred_set/help/thms/unin/EMPTY_UNION.doc
hol98/src/pred_set/help/thms/unin/INTER_ASSOC.doc
hol98/src/pred_set/help/thms/unin/INTER_COMM.doc
hol98/src/pred_set/help/thms/unin/INTER_DEF.doc
hol98/src/pred_set/help/thms/unin/INTER_EMPTY.doc
hol98/src/pred_set/help/thms/unin/INTER_IDEMPOT.doc
hol98/src/pred_set/help/thms/unin/INTER_OVER_UNION.doc
hol98/src/pred_set/help/thms/unin/INTER_SUBSET.doc
hol98/src/pred_set/help/thms/unin/INTER_UNIV.doc
hol98/src/pred_set/help/thms/unin/IN_INTER.doc
hol98/src/pred_set/help/thms/unin/IN_UNION.doc
hol98/src/pred_set/help/thms/unin/SUBSET_INTER_ABSORPTION.doc
hol98/src/pred_set/help/thms/unin/SUBSET_UNION.doc
hol98/src/pred_set/help/thms/unin/SUBSET_UNION_ABSORPTION.doc
hol98/src/pred_set/help/thms/unin/UNION_ASSOC.doc
hol98/src/pred_set/help/thms/unin/UNION_COMM.doc
hol98/src/pred_set/help/thms/unin/UNION_DEF.doc
hol98/src/pred_set/help/thms/unin/UNION_EMPTY.doc
hol98/src/pred_set/help/thms/unin/UNION_IDEMPOT.doc
hol98/src/pred_set/help/thms/unin/UNION_OVER_INTER.doc
hol98/src/pred_set/help/thms/unin/UNION_UNIV.doc
----------------------------------------------------------------------