bass% cd /local/scratch/mjcg/HOL98 bass% cvs -d:pserver:anonymous@cvs.sourceforge.net:/cvsroot/hol login (Logging in to anonymous@cvs.sourceforge.net) CVS password: (press RETURN when asked for a password) bass% cvs -z3 -d:pserver:anonymous@cvs.sourceforge.net:/cvsroot/hol co hol98 cvs server: Updating hol98 U hol98/COPYRIGHT U hol98/README U hol98/install.txt cvs server: Updating hol98/Manual U hol98/Manual/Makefile U hol98/Manual/READ-ME cvs server: Updating hol98/Manual/Covers U hol98/Manual/Covers/CRC.ps U hol98/Manual/Covers/DESCRIPTION.ps U hol98/Manual/Covers/LANTERN.ps U hol98/Manual/Covers/LIBRARIES.ps U hol98/Manual/Covers/Makefile U hol98/Manual/Covers/READ-ME U hol98/Manual/Covers/REFERENCE.ps U hol98/Manual/Covers/TUTORIAL.ps U hol98/Manual/Covers/arms.ps U hol98/Manual/Covers/dsto.ps U hol98/Manual/Covers/endpages.sty U hol98/Manual/Covers/endpages.tex U hol98/Manual/Covers/titlepages.sty U hol98/Manual/Covers/titlepages.tex cvs server: Updating hol98/Manual/Description U hol98/Manual/Description/.cvsignore U hol98/Manual/Description/Makefile U hol98/Manual/Description/conv.tex U hol98/Manual/Description/description.tex U hol98/Manual/Description/drules.tex U hol98/Manual/Description/hol98.dot U hol98/Manual/Description/hol98.pic U hol98/Manual/Description/libraries.tex U hol98/Manual/Description/logic.tex U hol98/Manual/Description/map.tex U hol98/Manual/Description/misc.tex U hol98/Manual/Description/preface.tex U hol98/Manual/Description/references.tex U hol98/Manual/Description/semantics.tex U hol98/Manual/Description/syntax.tex U hol98/Manual/Description/system.tex U hol98/Manual/Description/tactics.tex U hol98/Manual/Description/theories.tex U hol98/Manual/Description/title.tex U hol98/Manual/Description/version2.tex cvs server: Updating hol98/Manual/Guide U hol98/Manual/Guide/READ-ME U hol98/Manual/Guide/guide.tex cvs server: Updating hol98/Manual/LaTeX U hol98/Manual/LaTeX/READ-ME U hol98/Manual/LaTeX/ack.tex U hol98/Manual/LaTeX/commands.tex U hol98/Manual/LaTeX/cover_info.tex U hol98/Manual/LaTeX/layout.sty U hol98/Manual/LaTeX/layout.tex U hol98/Manual/LaTeX/pic-macros.tex U hol98/Manual/LaTeX/ref-macros.tex cvs server: Updating hol98/Manual/Reference U hol98/Manual/Reference/.cvsignore U hol98/Manual/Reference/Makefile U hol98/Manual/Reference/READ-ME U hol98/Manual/Reference/entries-intro.tex U hol98/Manual/Reference/preface.tex U hol98/Manual/Reference/reference.tex U hol98/Manual/Reference/theorems-intro.tex U hol98/Manual/Reference/title.tex cvs server: Updating hol98/Manual/Reference/bin U hol98/Manual/Reference/bin/doc-to-tex U hol98/Manual/Reference/bin/doc-to-tex.sed cvs server: Updating hol98/Manual/Tutorial U hol98/Manual/Tutorial/.cvsignore U hol98/Manual/Tutorial/Makefile U hol98/Manual/Tutorial/READ-ME U hol98/Manual/Tutorial/binomial-bib.tex U hol98/Manual/Tutorial/binomial.tex U hol98/Manual/Tutorial/combin.tex U hol98/Manual/Tutorial/euclid.tex U hol98/Manual/Tutorial/intro.tex U hol98/Manual/Tutorial/logic.tex U hol98/Manual/Tutorial/ml.tex U hol98/Manual/Tutorial/more-examples.tex U hol98/Manual/Tutorial/parity.tex U hol98/Manual/Tutorial/preface.tex U hol98/Manual/Tutorial/proof.tex U hol98/Manual/Tutorial/references.tex U hol98/Manual/Tutorial/theories.tex U hol98/Manual/Tutorial/title.tex U hol98/Manual/Tutorial/tool.tex U hol98/Manual/Tutorial/tutorial.hva U hol98/Manual/Tutorial/tutorial.tex cvs server: Updating hol98/Manual/Tutorial/binomial U hol98/Manual/Tutorial/binomial/appendix.tex U hol98/Manual/Tutorial/binomial/binomial.tex cvs server: Updating hol98/bin U hol98/bin/README cvs server: Updating hol98/developers U hol98/developers/TAGS-policy U hol98/developers/prettifier.pl U hol98/developers/releasing-hol cvs server: Updating hol98/developers/help U hol98/developers/help/Database.sig U hol98/developers/help/Database.sml U hol98/developers/help/Lexer.lex U hol98/developers/help/Makefile U hol98/developers/help/Parser.grm U hol98/developers/help/Parsspec.sml U hol98/developers/help/README U hol98/developers/help/clean-adocs.sh U hol98/developers/help/gen-adoc.sed U hol98/developers/help/gen-adocs.sh U hol98/developers/help/mk_dbs.sml cvs server: Updating hol98/doc U hol98/doc/changes U hol98/doc/faq.tmpl U hol98/doc/kananaskis-1.release U hol98/doc/taupo-1.release U hol98/doc/taupo-2.release U hol98/doc/taupo-3.release U hol98/doc/taupo-4.release U hol98/doc/taupo-5.release cvs server: Updating hol98/doc/athabasca U hol98/doc/athabasca/Compare U hol98/doc/athabasca/athabasca.announce U hol98/doc/athabasca/athabasca.dot U hol98/doc/athabasca/athabasca.release U hol98/doc/athabasca/changes cvs server: Updating hol98/doc/hol-mode U hol98/doc/hol-mode/Makefile U hol98/doc/hol-mode/hol-mode.tex cvs server: Updating hol98/doc/manual cvs server: Updating hol98/examples U hol98/examples/README U hol98/examples/Thery.sml U hol98/examples/autopilot.sml U hol98/examples/euclid.sml U hol98/examples/fol.sml U hol98/examples/taut.sml U hol98/examples/tempScript.sml cvs server: Updating hol98/examples/MLsyntax U hol98/examples/MLsyntax/MLScript.sml U hol98/examples/MLsyntax/README cvs server: Updating hol98/examples/RSA U hol98/examples/RSA/binomialScript.sml U hol98/examples/RSA/congruentScript.sml U hol98/examples/RSA/dividesScript.sml U hol98/examples/RSA/factorialScript.sml U hol98/examples/RSA/fermatScript.sml U hol98/examples/RSA/gcdScript.sml U hol98/examples/RSA/powerScript.sml U hol98/examples/RSA/primeScript.sml U hol98/examples/RSA/rsaScript.sml U hol98/examples/RSA/summationScript.sml cvs server: Updating hol98/examples/bmark U hol98/examples/bmark/Bmark.sml U hol98/examples/bmark/Readme U hol98/examples/bmark/run_bmark cvs server: Updating hol98/examples/ind_def U hol98/examples/ind_def/algebraScript.sml U hol98/examples/ind_def/clScript.sml U hol98/examples/ind_def/milScript.sml U hol98/examples/ind_def/opsemScript.sml cvs server: Updating hol98/examples/lambda U hol98/examples/lambda/dBScript.sml U hol98/examples/lambda/ncScript.sml cvs server: Updating hol98/examples/parity U hol98/examples/parity/PARITY.sml cvs server: Updating hol98/help U hol98/help/template cvs server: Updating hol98/help/Docfiles U hol98/help/Docfiles/##.doc U hol98/help/Docfiles/++.doc U hol98/help/Docfiles/A.doc U hol98/help/Docfiles/ABS.doc U hol98/help/Docfiles/ABS_CONV.doc U hol98/help/Docfiles/ACCEPT_TAC.doc U hol98/help/Docfiles/AC_CONV.doc U hol98/help/Docfiles/ADD_ASSUM.doc U hol98/help/Docfiles/ALL_CONV.doc U hol98/help/Docfiles/ALL_TAC.doc U hol98/help/Docfiles/ALL_THEN.doc U hol98/help/Docfiles/ALPHA.doc U hol98/help/Docfiles/ALPHA_CONV.doc U hol98/help/Docfiles/AND_EXISTS_CONV.doc U hol98/help/Docfiles/AND_FORALL_CONV.doc U hol98/help/Docfiles/ANTE_CONJ_CONV.doc U hol98/help/Docfiles/ANTE_RES_THEN.doc U hol98/help/Docfiles/AP_TERM.doc U hol98/help/Docfiles/AP_TERM_TAC.doc U hol98/help/Docfiles/AP_THM.doc U hol98/help/Docfiles/AP_THM_TAC.doc U hol98/help/Docfiles/ASM_CASES_TAC.doc U hol98/help/Docfiles/ASM_MESON_TAC.doc U hol98/help/Docfiles/ASM_REWRITE_RULE.doc U hol98/help/Docfiles/ASM_REWRITE_TAC.doc U hol98/help/Docfiles/ASM_SIMP_RULE.doc U hol98/help/Docfiles/ASM_SIMP_TAC.doc U hol98/help/Docfiles/ASSUME.doc U hol98/help/Docfiles/ASSUME_TAC.doc U hol98/help/Docfiles/ASSUM_LIST.doc U hol98/help/Docfiles/Absyn.doc U hol98/help/Docfiles/B.doc U hol98/help/Docfiles/BETA_CONV.doc U hol98/help/Docfiles/BETA_RULE.doc U hol98/help/Docfiles/BETA_TAC.doc U hol98/help/Docfiles/BINOP_CONV.doc U hol98/help/Docfiles/BODY_CONJUNCTS.doc U hol98/help/Docfiles/BOOL_CASES_TAC.doc U hol98/help/Docfiles/C.doc U hol98/help/Docfiles/CASES_THENL.doc U hol98/help/Docfiles/CBV_CONV.doc U hol98/help/Docfiles/CCONTR.doc U hol98/help/Docfiles/CCONTR_TAC.doc U hol98/help/Docfiles/CHANGED_CONV.doc U hol98/help/Docfiles/CHANGED_TAC.doc U hol98/help/Docfiles/CHECK_ASSUME_TAC.doc U hol98/help/Docfiles/CHOOSE.doc U hol98/help/Docfiles/CHOOSE_TAC.doc U hol98/help/Docfiles/CHOOSE_THEN.doc U hol98/help/Docfiles/COND_CASES_TAC.doc U hol98/help/Docfiles/COND_CONV.doc U hol98/help/Docfiles/CONJ.doc U hol98/help/Docfiles/CONJUNCT1.doc U hol98/help/Docfiles/CONJUNCT2.doc U hol98/help/Docfiles/CONJUNCTS.doc U hol98/help/Docfiles/CONJUNCTS_CONV.doc U hol98/help/Docfiles/CONJUNCTS_THEN.doc U hol98/help/Docfiles/CONJUNCTS_THEN2.doc U hol98/help/Docfiles/CONJ_DISCH.doc U hol98/help/Docfiles/CONJ_DISCHL.doc U hol98/help/Docfiles/CONJ_LIST.doc U hol98/help/Docfiles/CONJ_PAIR.doc U hol98/help/Docfiles/CONJ_SET_CONV.doc U hol98/help/Docfiles/CONJ_TAC.doc U hol98/help/Docfiles/CONTR.doc U hol98/help/Docfiles/CONTRAPOS.doc U hol98/help/Docfiles/CONTRAPOS_CONV.doc U hol98/help/Docfiles/CONTR_TAC.doc U hol98/help/Docfiles/CONV_RULE.doc U hol98/help/Docfiles/CONV_TAC.doc U hol98/help/Docfiles/Cases.doc U hol98/help/Docfiles/DEPTH_CONV.doc U hol98/help/Docfiles/DISCARD_TAC.doc U hol98/help/Docfiles/DISCH.doc U hol98/help/Docfiles/DISCH_ALL.doc U hol98/help/Docfiles/DISCH_TAC.doc U hol98/help/Docfiles/DISCH_THEN.doc U hol98/help/Docfiles/DISJ1.doc U hol98/help/Docfiles/DISJ1_TAC.doc U hol98/help/Docfiles/DISJ2.doc U hol98/help/Docfiles/DISJ2_TAC.doc U hol98/help/Docfiles/DISJ_CASES.doc U hol98/help/Docfiles/DISJ_CASES_TAC.doc U hol98/help/Docfiles/DISJ_CASES_THEN.doc U hol98/help/Docfiles/DISJ_CASES_THEN2.doc U hol98/help/Docfiles/DISJ_CASES_THENL.doc U hol98/help/Docfiles/DISJ_CASES_UNION.doc U hol98/help/Docfiles/DISJ_IMP.doc U hol98/help/Docfiles/Define.doc U hol98/help/Docfiles/EQF_ELIM.doc U hol98/help/Docfiles/EQF_INTRO.doc U hol98/help/Docfiles/EQT_ELIM.doc U hol98/help/Docfiles/EQT_INTRO.doc U hol98/help/Docfiles/EQ_IMP_RULE.doc U hol98/help/Docfiles/EQ_MP.doc U hol98/help/Docfiles/EQ_TAC.doc U hol98/help/Docfiles/ERR_outstream.doc U hol98/help/Docfiles/ERR_to_string.doc U hol98/help/Docfiles/ETA_CONV.doc U hol98/help/Docfiles/EVERY.doc U hol98/help/Docfiles/EVERY_ASSUM.doc U hol98/help/Docfiles/EVERY_CONJ_CONV.doc U hol98/help/Docfiles/EVERY_CONV.doc U hol98/help/Docfiles/EVERY_DISJ_CONV.doc U hol98/help/Docfiles/EVERY_TCL.doc U hol98/help/Docfiles/EXISTENCE.doc U hol98/help/Docfiles/EXISTS.doc U hol98/help/Docfiles/EXISTS_AND_CONV.doc U hol98/help/Docfiles/EXISTS_EQ.doc U hol98/help/Docfiles/EXISTS_IMP.doc U hol98/help/Docfiles/EXISTS_IMP_CONV.doc U hol98/help/Docfiles/EXISTS_NOT_CONV.doc U hol98/help/Docfiles/EXISTS_OR_CONV.doc U hol98/help/Docfiles/EXISTS_TAC.doc U hol98/help/Docfiles/EXISTS_UNIQUE_CONV.doc U hol98/help/Docfiles/EXT.doc U hol98/help/Docfiles/F.doc U hol98/help/Docfiles/FAIL_TAC.doc U hol98/help/Docfiles/FILTER_ASM_REWRITE_RULE.doc U hol98/help/Docfiles/FILTER_ASM_REWRITE_TAC.doc U hol98/help/Docfiles/FILTER_DISCH_TAC.doc U hol98/help/Docfiles/FILTER_DISCH_THEN.doc U hol98/help/Docfiles/FILTER_GEN_TAC.doc U hol98/help/Docfiles/FILTER_ONCE_ASM_REWRITE_RULE.doc U hol98/help/Docfiles/FILTER_ONCE_ASM_REWRITE_TAC.doc U hol98/help/Docfiles/FILTER_PURE_ASM_REWRITE_RULE.doc U hol98/help/Docfiles/FILTER_PURE_ASM_REWRITE_TAC.doc U hol98/help/Docfiles/FILTER_PURE_ONCE_ASM_REWRITE_RULE.doc U hol98/help/Docfiles/FILTER_PURE_ONCE_ASM_REWRITE_TAC.doc U hol98/help/Docfiles/FILTER_STRIP_TAC.doc U hol98/help/Docfiles/FILTER_STRIP_THEN.doc U hol98/help/Docfiles/FIRST.doc U hol98/help/Docfiles/FIRST_ASSUM.doc U hol98/help/Docfiles/FIRST_CONV.doc U hol98/help/Docfiles/FIRST_TCL.doc U hol98/help/Docfiles/FIRST_X_ASSUM.doc U hol98/help/Docfiles/FORALL_AND_CONV.doc U hol98/help/Docfiles/FORALL_EQ.doc U hol98/help/Docfiles/FORALL_IMP_CONV.doc U hol98/help/Docfiles/FORALL_NOT_CONV.doc U hol98/help/Docfiles/FORALL_OR_CONV.doc U hol98/help/Docfiles/FORK_CONV.doc U hol98/help/Docfiles/FREEZE_THEN.doc U hol98/help/Docfiles/FRONT_CONJ_CONV.doc U hol98/help/Docfiles/FULL_SIMP_TAC.doc U hol98/help/Docfiles/FUN_EQ_CONV.doc U hol98/help/Docfiles/Feedback.doc U hol98/help/Docfiles/GEN.doc U hol98/help/Docfiles/GENL.doc U hol98/help/Docfiles/GEN_ALL.doc U hol98/help/Docfiles/GEN_ALPHA_CONV.doc U hol98/help/Docfiles/GEN_BETA_CONV.doc U hol98/help/Docfiles/GEN_MESON_TAC.doc U hol98/help/Docfiles/GEN_REWRITE_CONV.doc U hol98/help/Docfiles/GEN_REWRITE_RULE.doc U hol98/help/Docfiles/GEN_REWRITE_TAC.doc U hol98/help/Docfiles/GEN_TAC.doc U hol98/help/Docfiles/GSPEC.doc U hol98/help/Docfiles/GSUBST_TAC.doc U hol98/help/Docfiles/GSYM.doc U hol98/help/Docfiles/HALF_MK_ABS.doc U hol98/help/Docfiles/HOL_ERR.doc U hol98/help/Docfiles/HOL_MESG.doc U hol98/help/Docfiles/HOL_WARNING.doc U hol98/help/Docfiles/Hol_defn.doc U hol98/help/Docfiles/Hol_reln.doc U hol98/help/Docfiles/I.doc U hol98/help/Docfiles/IMP_ANTISYM_RULE.doc U hol98/help/Docfiles/IMP_CANON.doc U hol98/help/Docfiles/IMP_CONJ.doc U hol98/help/Docfiles/IMP_ELIM.doc U hol98/help/Docfiles/IMP_RES_TAC.doc U hol98/help/Docfiles/IMP_RES_THEN.doc U hol98/help/Docfiles/IMP_TRANS.doc U hol98/help/Docfiles/INDUCT.doc U hol98/help/Docfiles/INDUCT_TAC.doc U hol98/help/Docfiles/INDUCT_THEN.doc U hol98/help/Docfiles/INST.doc U hol98/help/Docfiles/INST_TYPE.doc U hol98/help/Docfiles/INST_TY_TERM.doc U hol98/help/Docfiles/ISPEC.doc U hol98/help/Docfiles/ISPECL.doc U hol98/help/Docfiles/Induct-lc.doc U hol98/help/Docfiles/K.doc U hol98/help/Docfiles/LAND_CONV.doc U hol98/help/Docfiles/LEFT_AND_EXISTS_CONV.doc U hol98/help/Docfiles/LEFT_AND_FORALL_CONV.doc U hol98/help/Docfiles/LEFT_IMP_EXISTS_CONV.doc U hol98/help/Docfiles/LEFT_IMP_FORALL_CONV.doc U hol98/help/Docfiles/LEFT_OR_EXISTS_CONV.doc U hol98/help/Docfiles/LEFT_OR_FORALL_CONV.doc U hol98/help/Docfiles/LIST_BETA_CONV.doc U hol98/help/Docfiles/LIST_CONJ.doc U hol98/help/Docfiles/LIST_INDUCT.doc U hol98/help/Docfiles/LIST_INDUCT_TAC.doc U hol98/help/Docfiles/LIST_MK_EXISTS.doc U hol98/help/Docfiles/LIST_MP.doc U hol98/help/Docfiles/MAP_EVERY.doc U hol98/help/Docfiles/MAP_FIRST.doc U hol98/help/Docfiles/MATCH_ACCEPT_TAC.doc U hol98/help/Docfiles/MATCH_MP.doc U hol98/help/Docfiles/MATCH_MP_TAC.doc U hol98/help/Docfiles/MESG_outstream.doc U hol98/help/Docfiles/MESG_to_string.doc U hol98/help/Docfiles/MESON_TAC.doc U hol98/help/Docfiles/MK_ABS.doc U hol98/help/Docfiles/MK_COMB.doc U hol98/help/Docfiles/MK_EXISTS.doc U hol98/help/Docfiles/MP.doc U hol98/help/Docfiles/MP_TAC.doc U hol98/help/Docfiles/NEG_DISCH.doc U hol98/help/Docfiles/NOT_ELIM.doc U hol98/help/Docfiles/NOT_EQ_SYM.doc U hol98/help/Docfiles/NOT_EXISTS_CONV.doc U hol98/help/Docfiles/NOT_FORALL_CONV.doc U hol98/help/Docfiles/NOT_INTRO.doc U hol98/help/Docfiles/NO_CONV.doc U hol98/help/Docfiles/NO_TAC.doc U hol98/help/Docfiles/NO_THEN.doc U hol98/help/Docfiles/ONCE_ASM_REWRITE_RULE.doc U hol98/help/Docfiles/ONCE_ASM_REWRITE_TAC.doc U hol98/help/Docfiles/ONCE_DEPTH_CONV.doc U hol98/help/Docfiles/ONCE_REWRITE_CONV.doc U hol98/help/Docfiles/ONCE_REWRITE_RULE.doc U hol98/help/Docfiles/ONCE_REWRITE_TAC.doc U hol98/help/Docfiles/ORELSE.doc U hol98/help/Docfiles/ORELSEC.doc U hol98/help/Docfiles/ORELSE_TCL.doc U hol98/help/Docfiles/OR_EXISTS_CONV.doc U hol98/help/Docfiles/OR_FORALL_CONV.doc U hol98/help/Docfiles/PAIRED_BETA_CONV.doc U hol98/help/Docfiles/PAIRED_ETA_CONV.doc U hol98/help/Docfiles/PART_MATCH.doc U hol98/help/Docfiles/PAT_ASSUM.doc U hol98/help/Docfiles/POP_ASSUM.doc U hol98/help/Docfiles/POP_ASSUM_LIST.doc U hol98/help/Docfiles/PROVE.doc U hol98/help/Docfiles/PROVE_HYP.doc U hol98/help/Docfiles/PURE_ASM_REWRITE_RULE.doc U hol98/help/Docfiles/PURE_ASM_REWRITE_TAC.doc U hol98/help/Docfiles/PURE_ONCE_ASM_REWRITE_RULE.doc U hol98/help/Docfiles/PURE_ONCE_ASM_REWRITE_TAC.doc U hol98/help/Docfiles/PURE_ONCE_REWRITE_CONV.doc U hol98/help/Docfiles/PURE_ONCE_REWRITE_RULE.doc U hol98/help/Docfiles/PURE_ONCE_REWRITE_TAC.doc U hol98/help/Docfiles/PURE_REWRITE_CONV.doc U hol98/help/Docfiles/PURE_REWRITE_RULE.doc U hol98/help/Docfiles/PURE_REWRITE_TAC.doc U hol98/help/Docfiles/Psyntax.doc U hol98/help/Docfiles/RAND_CONV.doc U hol98/help/Docfiles/RATOR_CONV.doc U hol98/help/Docfiles/README.Hol98 U hol98/help/Docfiles/REDEPTH_CONV.doc U hol98/help/Docfiles/REFINE_EXISTS_TAC.doc U hol98/help/Docfiles/REFL.doc U hol98/help/Docfiles/REFL_TAC.doc U hol98/help/Docfiles/RENAME_VARS_CONV.doc U hol98/help/Docfiles/REPEAT.doc U hol98/help/Docfiles/REPEATC.doc U hol98/help/Docfiles/REPEAT_GTCL.doc U hol98/help/Docfiles/REPEAT_TCL.doc U hol98/help/Docfiles/RES_CANON.doc U hol98/help/Docfiles/RES_TAC.doc U hol98/help/Docfiles/RES_THEN.doc U hol98/help/Docfiles/REWRITE_CONV.doc U hol98/help/Docfiles/REWRITE_RULE.doc U hol98/help/Docfiles/REWRITE_TAC.doc U hol98/help/Docfiles/REWR_CONV.doc U hol98/help/Docfiles/RIGHT_AND_EXISTS_CONV.doc U hol98/help/Docfiles/RIGHT_AND_FORALL_CONV.doc U hol98/help/Docfiles/RIGHT_BETA.doc U hol98/help/Docfiles/RIGHT_CONV_RULE.doc U hol98/help/Docfiles/RIGHT_IMP_EXISTS_CONV.doc U hol98/help/Docfiles/RIGHT_IMP_FORALL_CONV.doc U hol98/help/Docfiles/RIGHT_LIST_BETA.doc U hol98/help/Docfiles/RIGHT_OR_EXISTS_CONV.doc U hol98/help/Docfiles/RIGHT_OR_FORALL_CONV.doc U hol98/help/Docfiles/RULE_ASSUM_TAC.doc U hol98/help/Docfiles/Raise.doc U hol98/help/Docfiles/Rsyntax.doc U hol98/help/Docfiles/S.doc U hol98/help/Docfiles/SELECT_CONV.doc U hol98/help/Docfiles/SELECT_ELIM.doc U hol98/help/Docfiles/SELECT_EQ.doc U hol98/help/Docfiles/SELECT_INTRO.doc U hol98/help/Docfiles/SELECT_RULE.doc U hol98/help/Docfiles/SIMPSET.doc U hol98/help/Docfiles/SIMP_CONV.doc U hol98/help/Docfiles/SIMP_PROVE.doc U hol98/help/Docfiles/SIMP_RULE.doc U hol98/help/Docfiles/SIMP_TAC.doc U hol98/help/Docfiles/SKOLEM_CONV.doc U hol98/help/Docfiles/SPEC.doc U hol98/help/Docfiles/SPECL.doc U hol98/help/Docfiles/SPEC_ALL.doc U hol98/help/Docfiles/SPEC_TAC.doc U hol98/help/Docfiles/SPEC_VAR.doc U hol98/help/Docfiles/STRIP_ASSUME_TAC.doc U hol98/help/Docfiles/STRIP_GOAL_THEN.doc U hol98/help/Docfiles/STRIP_TAC.doc U hol98/help/Docfiles/STRIP_THM_THEN.doc U hol98/help/Docfiles/STRUCT_CASES_TAC.doc U hol98/help/Docfiles/SUBGOAL_THEN.doc U hol98/help/Docfiles/SUBS.doc U hol98/help/Docfiles/SUBST.doc U hol98/help/Docfiles/SUBST1_TAC.doc U hol98/help/Docfiles/SUBST_ALL_TAC.doc U hol98/help/Docfiles/SUBST_CONV.doc U hol98/help/Docfiles/SUBST_MATCH.doc U hol98/help/Docfiles/SUBST_OCCS_TAC.doc U hol98/help/Docfiles/SUBST_TAC.doc U hol98/help/Docfiles/SUBS_OCCS.doc U hol98/help/Docfiles/SUB_CONV.doc U hol98/help/Docfiles/SWAP_EXISTS_CONV.doc U hol98/help/Docfiles/SYM.doc U hol98/help/Docfiles/SYM_CONV.doc U hol98/help/Docfiles/T.doc U hol98/help/Docfiles/TAC_PROOF.doc U hol98/help/Docfiles/THEN.doc U hol98/help/Docfiles/THENC.doc U hol98/help/Docfiles/THENL.doc U hol98/help/Docfiles/THEN_TCL.doc U hol98/help/Docfiles/TOP_DEPTH_CONV.doc U hol98/help/Docfiles/TRANS.doc U hol98/help/Docfiles/TRY.doc U hol98/help/Docfiles/TRY_CONV.doc U hol98/help/Docfiles/Term.doc U hol98/help/Docfiles/UNDISCH.doc U hol98/help/Docfiles/UNDISCH_ALL.doc U hol98/help/Docfiles/UNDISCH_TAC.doc U hol98/help/Docfiles/UNDISCH_THEN.doc U hol98/help/Docfiles/W.doc U hol98/help/Docfiles/WARNING_outstream.doc U hol98/help/Docfiles/WARNING_to_string.doc U hol98/help/Docfiles/WF_REL_TAC.doc U hol98/help/Docfiles/X_CASES_THEN.doc U hol98/help/Docfiles/X_CASES_THENL.doc U hol98/help/Docfiles/X_CHOOSE_TAC.doc U hol98/help/Docfiles/X_CHOOSE_THEN.doc U hol98/help/Docfiles/X_FUN_EQ_CONV.doc U hol98/help/Docfiles/X_GEN_TAC.doc U hol98/help/Docfiles/X_SKOLEM_CONV.doc U hol98/help/Docfiles/aconv.doc U hol98/help/Docfiles/add_bare_numeral_form.doc U hol98/help/Docfiles/add_implicit_rewrites.doc U hol98/help/Docfiles/add_infix.doc U hol98/help/Docfiles/add_listform.doc U hol98/help/Docfiles/add_numeral_form.doc U hol98/help/Docfiles/add_rewrites.doc U hol98/help/Docfiles/add_rule.doc U hol98/help/Docfiles/add_user_printer.doc U hol98/help/Docfiles/all.doc U hol98/help/Docfiles/all2.doc U hol98/help/Docfiles/allowed_term_constant.doc U hol98/help/Docfiles/allowed_type_constant.doc U hol98/help/Docfiles/alpha.doc U hol98/help/Docfiles/ancestry.doc U hol98/help/Docfiles/append.doc U hol98/help/Docfiles/arb.doc U hol98/help/Docfiles/arity.doc U hol98/help/Docfiles/assert.doc U hol98/help/Docfiles/assert_exn.doc U hol98/help/Docfiles/assoc.doc U hol98/help/Docfiles/assoc1.doc U hol98/help/Docfiles/assoc2.doc U hol98/help/Docfiles/associate_restriction.doc U hol98/help/Docfiles/axiom.doc U hol98/help/Docfiles/axioms.doc U hol98/help/Docfiles/b-lc.doc U hol98/help/Docfiles/backup.doc U hol98/help/Docfiles/beta.doc U hol98/help/Docfiles/binder_restrictions.doc U hol98/help/Docfiles/binders.doc U hol98/help/Docfiles/body.doc U hol98/help/Docfiles/bool.doc U hol98/help/Docfiles/bool_EQ_CONV.doc U hol98/help/Docfiles/bool_case.doc U hol98/help/Docfiles/bool_rewrites.doc U hol98/help/Docfiles/bool_ss.doc U hol98/help/Docfiles/butlast.doc U hol98/help/Docfiles/bvar.doc U hol98/help/Docfiles/can.doc U hol98/help/Docfiles/clear_overloads_on.doc U hol98/help/Docfiles/clear_prefs_for_term.doc U hol98/help/Docfiles/combine.doc U hol98/help/Docfiles/concat.doc U hol98/help/Docfiles/concl.doc U hol98/help/Docfiles/conditional.doc U hol98/help/Docfiles/conjunction.doc U hol98/help/Docfiles/conjuncts-lc.doc U hol98/help/Docfiles/cons.doc U hol98/help/Docfiles/constants.doc U hol98/help/Docfiles/current_theory.doc U hol98/help/Docfiles/current_trace.doc U hol98/help/Docfiles/curry.doc U hol98/help/Docfiles/define_new_type_bijections.doc U hol98/help/Docfiles/define_type.doc U hol98/help/Docfiles/delete_restriction.doc U hol98/help/Docfiles/delta.doc U hol98/help/Docfiles/dest_abs.doc U hol98/help/Docfiles/dest_arb.doc U hol98/help/Docfiles/dest_bool_case.doc U hol98/help/Docfiles/dest_comb.doc U hol98/help/Docfiles/dest_cond.doc U hol98/help/Docfiles/dest_conj.doc U hol98/help/Docfiles/dest_cons.doc U hol98/help/Docfiles/dest_const.doc U hol98/help/Docfiles/dest_disj.doc U hol98/help/Docfiles/dest_eq.doc U hol98/help/Docfiles/dest_eq_ty.doc U hol98/help/Docfiles/dest_exists.doc U hol98/help/Docfiles/dest_exists1.doc U hol98/help/Docfiles/dest_forall.doc U hol98/help/Docfiles/dest_imp.doc U hol98/help/Docfiles/dest_imp_only.doc U hol98/help/Docfiles/dest_let.doc U hol98/help/Docfiles/dest_list.doc U hol98/help/Docfiles/dest_neg.doc U hol98/help/Docfiles/dest_pabs.doc U hol98/help/Docfiles/dest_pair.doc U hol98/help/Docfiles/dest_select.doc U hol98/help/Docfiles/dest_thm.doc U hol98/help/Docfiles/dest_thy_const.doc U hol98/help/Docfiles/dest_thy_type.doc U hol98/help/Docfiles/dest_type.doc U hol98/help/Docfiles/dest_var.doc U hol98/help/Docfiles/dest_vartype.doc U hol98/help/Docfiles/disch-lc.doc U hol98/help/Docfiles/disjunction.doc U hol98/help/Docfiles/disjuncts.doc U hol98/help/Docfiles/dom_rng.doc U hol98/help/Docfiles/e.doc U hol98/help/Docfiles/el.doc U hol98/help/Docfiles/emit_ERR.doc U hol98/help/Docfiles/emit_MESG.doc U hol98/help/Docfiles/emit_WARNING.doc U hol98/help/Docfiles/empty_rewrites.doc U hol98/help/Docfiles/end_itlist.doc U hol98/help/Docfiles/enumerate.doc U hol98/help/Docfiles/equal.doc U hol98/help/Docfiles/equality.doc U hol98/help/Docfiles/error_record.doc U hol98/help/Docfiles/existential.doc U hol98/help/Docfiles/exists-lc.doc U hol98/help/Docfiles/exists.doc U hol98/help/Docfiles/exists1.doc U hol98/help/Docfiles/exn_to_string.doc U hol98/help/Docfiles/expand.doc U hol98/help/Docfiles/expandf.doc U hol98/help/Docfiles/fail.doc U hol98/help/Docfiles/failwith.doc U hol98/help/Docfiles/filter.doc U hol98/help/Docfiles/find.doc U hol98/help/Docfiles/first-lc.doc U hol98/help/Docfiles/first.doc U hol98/help/Docfiles/flatten.doc U hol98/help/Docfiles/format_ERR.doc U hol98/help/Docfiles/format_MESG.doc U hol98/help/Docfiles/format_WARNING.doc U hol98/help/Docfiles/free_in.doc U hol98/help/Docfiles/frees.doc U hol98/help/Docfiles/freesl.doc U hol98/help/Docfiles/front_last.doc U hol98/help/Docfiles/fst.doc U hol98/help/Docfiles/funpow.doc U hol98/help/Docfiles/g.doc U hol98/help/Docfiles/gamma.doc U hol98/help/Docfiles/gather.doc U hol98/help/Docfiles/gen_tyvar.doc U hol98/help/Docfiles/genvar.doc U hol98/help/Docfiles/hidden.doc U hol98/help/Docfiles/hide.doc U hol98/help/Docfiles/hol_ss.doc U hol98/help/Docfiles/hyp.doc U hol98/help/Docfiles/hyp_union.doc U hol98/help/Docfiles/implication.doc U hol98/help/Docfiles/implicit_rewrites.doc U hol98/help/Docfiles/ind.doc U hol98/help/Docfiles/index.doc U hol98/help/Docfiles/initial_rws.doc U hol98/help/Docfiles/inst-lc.doc U hol98/help/Docfiles/int_of_string.doc U hol98/help/Docfiles/intersect.doc U hol98/help/Docfiles/is_abs.doc U hol98/help/Docfiles/is_arb.doc U hol98/help/Docfiles/is_axiom.doc U hol98/help/Docfiles/is_bool_case.doc U hol98/help/Docfiles/is_comb.doc U hol98/help/Docfiles/is_cond.doc U hol98/help/Docfiles/is_conj.doc U hol98/help/Docfiles/is_cons.doc U hol98/help/Docfiles/is_const.doc U hol98/help/Docfiles/is_constant.doc U hol98/help/Docfiles/is_disj.doc U hol98/help/Docfiles/is_eq.doc U hol98/help/Docfiles/is_exists.doc U hol98/help/Docfiles/is_exists1.doc U hol98/help/Docfiles/is_forall.doc U hol98/help/Docfiles/is_hidden.doc U hol98/help/Docfiles/is_imp.doc U hol98/help/Docfiles/is_imp_only.doc U hol98/help/Docfiles/is_let.doc U hol98/help/Docfiles/is_list.doc U hol98/help/Docfiles/is_neg.doc U hol98/help/Docfiles/is_pabs.doc U hol98/help/Docfiles/is_pair.doc U hol98/help/Docfiles/is_select.doc U hol98/help/Docfiles/is_type.doc U hol98/help/Docfiles/is_var.doc U hol98/help/Docfiles/is_vartype.doc U hol98/help/Docfiles/itlist.doc U hol98/help/Docfiles/itlist2.doc U hol98/help/Docfiles/known_constants.doc U hol98/help/Docfiles/last.doc U hol98/help/Docfiles/let_tm.doc U hol98/help/Docfiles/lhs.doc U hol98/help/Docfiles/list_mk_abs.doc U hol98/help/Docfiles/list_mk_comb.doc U hol98/help/Docfiles/list_mk_conj.doc U hol98/help/Docfiles/list_mk_disj.doc U hol98/help/Docfiles/list_mk_exists-lc.doc U hol98/help/Docfiles/list_mk_forall.doc U hol98/help/Docfiles/list_mk_fun.doc U hol98/help/Docfiles/list_mk_imp.doc U hol98/help/Docfiles/list_mk_pair.doc U hol98/help/Docfiles/list_of_binders.doc U hol98/help/Docfiles/map2.doc U hol98/help/Docfiles/mapfilter.doc U hol98/help/Docfiles/match_term.doc U hol98/help/Docfiles/match_type.doc U hol98/help/Docfiles/max_print_depth.doc U hol98/help/Docfiles/mem.doc U hol98/help/Docfiles/mk_HOL_ERR.doc U hol98/help/Docfiles/mk_abs-lc.doc U hol98/help/Docfiles/mk_arb.doc U hol98/help/Docfiles/mk_bool_case.doc U hol98/help/Docfiles/mk_comb-lc.doc U hol98/help/Docfiles/mk_cond.doc U hol98/help/Docfiles/mk_conj.doc U hol98/help/Docfiles/mk_cons.doc U hol98/help/Docfiles/mk_const.doc U hol98/help/Docfiles/mk_disj.doc U hol98/help/Docfiles/mk_eq.doc U hol98/help/Docfiles/mk_exists-lc.doc U hol98/help/Docfiles/mk_exists.doc U hol98/help/Docfiles/mk_exists1.doc U hol98/help/Docfiles/mk_forall.doc U hol98/help/Docfiles/mk_imp.doc U hol98/help/Docfiles/mk_let.doc U hol98/help/Docfiles/mk_list.doc U hol98/help/Docfiles/mk_neg.doc U hol98/help/Docfiles/mk_pabs.doc U hol98/help/Docfiles/mk_pair.doc U hol98/help/Docfiles/mk_primed_var.doc U hol98/help/Docfiles/mk_select.doc U hol98/help/Docfiles/mk_simpset.doc U hol98/help/Docfiles/mk_thm.doc U hol98/help/Docfiles/mk_thy_const.doc U hol98/help/Docfiles/mk_thy_type.doc U hol98/help/Docfiles/mk_type.doc U hol98/help/Docfiles/mk_var.doc U hol98/help/Docfiles/mk_vartype.doc U hol98/help/Docfiles/negation.doc U hol98/help/Docfiles/new_axiom.doc U hol98/help/Docfiles/new_binder.doc U hol98/help/Docfiles/new_binder_definition.doc U hol98/help/Docfiles/new_constant.doc U hol98/help/Docfiles/new_definition.doc U hol98/help/Docfiles/new_gen_definition.doc U hol98/help/Docfiles/new_infix.doc U hol98/help/Docfiles/new_infix_prim_rec_definition.doc U hol98/help/Docfiles/new_infixl_definition.doc U hol98/help/Docfiles/new_infixr_definition.doc U hol98/help/Docfiles/new_list_rec_definition.doc U hol98/help/Docfiles/new_open_axiom.doc U hol98/help/Docfiles/new_prim_rec_definition.doc U hol98/help/Docfiles/new_recursive_definition.doc U hol98/help/Docfiles/new_specification.doc U hol98/help/Docfiles/new_theory.doc U hol98/help/Docfiles/new_type.doc U hol98/help/Docfiles/new_type_definition.doc U hol98/help/Docfiles/overload_on.doc U hol98/help/Docfiles/p.doc U hol98/help/Docfiles/pair.doc U hol98/help/Docfiles/parents.doc U hol98/help/Docfiles/parse_from_grammars.doc U hol98/help/Docfiles/parse_in_context.doc U hol98/help/Docfiles/partial.doc U hol98/help/Docfiles/partition.doc U hol98/help/Docfiles/pluck.doc U hol98/help/Docfiles/prefer_form_with_tok.doc U hol98/help/Docfiles/priming.doc U hol98/help/Docfiles/print_term.doc U hol98/help/Docfiles/prove-lc.doc U hol98/help/Docfiles/prove_abs_fn_one_one.doc U hol98/help/Docfiles/prove_abs_fn_onto.doc U hol98/help/Docfiles/prove_cases_thm.doc U hol98/help/Docfiles/prove_constructors_distinct.doc U hol98/help/Docfiles/prove_constructors_one_one.doc U hol98/help/Docfiles/prove_induction_thm.doc U hol98/help/Docfiles/prove_rec_fn_exists.doc U hol98/help/Docfiles/prove_rep_fn_one_one.doc U hol98/help/Docfiles/prove_rep_fn_onto.doc U hol98/help/Docfiles/prove_thm.doc U hol98/help/Docfiles/pure_ss.doc U hol98/help/Docfiles/r.doc U hol98/help/Docfiles/rand.doc U hol98/help/Docfiles/rator.doc U hol98/help/Docfiles/register_btrace.doc U hol98/help/Docfiles/register_ftrace.doc U hol98/help/Docfiles/register_trace.doc U hol98/help/Docfiles/remove_ovl_mapping.doc U hol98/help/Docfiles/remove_rules_for_term.doc U hol98/help/Docfiles/remove_termtok.doc U hol98/help/Docfiles/remove_user_printer.doc U hol98/help/Docfiles/repeat.doc U hol98/help/Docfiles/reset_trace.doc U hol98/help/Docfiles/reset_traces.doc U hol98/help/Docfiles/rev_assoc.doc U hol98/help/Docfiles/rev_itlist.doc U hol98/help/Docfiles/rev_itlist2.doc U hol98/help/Docfiles/reveal.doc U hol98/help/Docfiles/rewrites.doc U hol98/help/Docfiles/rhs.doc U hol98/help/Docfiles/save_thm.doc U hol98/help/Docfiles/select.doc U hol98/help/Docfiles/set_backup.doc U hol98/help/Docfiles/set_fixity.doc U hol98/help/Docfiles/set_goal.doc U hol98/help/Docfiles/set_implicit_rewrites.doc U hol98/help/Docfiles/set_known_constants.doc U hol98/help/Docfiles/set_trace.doc U hol98/help/Docfiles/setify.doc U hol98/help/Docfiles/show_numeral_types.doc U hol98/help/Docfiles/show_types.doc U hol98/help/Docfiles/snd.doc U hol98/help/Docfiles/sort.doc U hol98/help/Docfiles/split.doc U hol98/help/Docfiles/split_after.doc U hol98/help/Docfiles/store_thm.doc U hol98/help/Docfiles/string_of_int.doc U hol98/help/Docfiles/strip_abs.doc U hol98/help/Docfiles/strip_comb.doc U hol98/help/Docfiles/strip_conj.doc U hol98/help/Docfiles/strip_disj.doc U hol98/help/Docfiles/strip_exists.doc U hol98/help/Docfiles/strip_forall.doc U hol98/help/Docfiles/strip_fun.doc U hol98/help/Docfiles/strip_imp.doc U hol98/help/Docfiles/strip_imp_only.doc U hol98/help/Docfiles/strip_neg.doc U hol98/help/Docfiles/strip_pair.doc U hol98/help/Docfiles/subst-lc.doc U hol98/help/Docfiles/subst_occs.doc U hol98/help/Docfiles/subtract.doc U hol98/help/Docfiles/term_grammar.doc U hol98/help/Docfiles/term_lt.doc U hol98/help/Docfiles/term_to_string.doc U hol98/help/Docfiles/tgoal.doc U hol98/help/Docfiles/thm_count.doc U hol98/help/Docfiles/top_goal.doc U hol98/help/Docfiles/top_thm.doc U hol98/help/Docfiles/total.doc U hol98/help/Docfiles/tprove.doc U hol98/help/Docfiles/trace.doc U hol98/help/Docfiles/traces.doc U hol98/help/Docfiles/try.doc U hol98/help/Docfiles/trye.doc U hol98/help/Docfiles/tryfind.doc U hol98/help/Docfiles/type_abbrev.doc U hol98/help/Docfiles/type_in.doc U hol98/help/Docfiles/type_in_type.doc U hol98/help/Docfiles/type_lt.doc U hol98/help/Docfiles/type_of.doc U hol98/help/Docfiles/type_subst.doc U hol98/help/Docfiles/type_tyvars.doc U hol98/help/Docfiles/types.doc U hol98/help/Docfiles/tyvars.doc U hol98/help/Docfiles/tyvarsl.doc U hol98/help/Docfiles/uncurry.doc U hol98/help/Docfiles/union.doc U hol98/help/Docfiles/universal.doc U hol98/help/Docfiles/unzip.doc U hol98/help/Docfiles/update_overload_maps.doc U hol98/help/Docfiles/variant.doc U hol98/help/Docfiles/version.doc U hol98/help/Docfiles/with_exn.doc U hol98/help/Docfiles/with_flag.doc U hol98/help/Docfiles/words.doc U hol98/help/Docfiles/words2.doc U hol98/help/Docfiles/wrap_exn.doc U hol98/help/Docfiles/xDefine.doc U hol98/help/Docfiles/zip.doc cvs server: Updating hol98/help/src U hol98/help/src/Asynt.sml U hol98/help/src/Database.sig U hol98/help/src/Database.sml U hol98/help/src/Doc2Html.sml U hol98/help/src/HOLPage.sml U hol98/help/src/Hasht.sig U hol98/help/src/Hasht.sml U hol98/help/src/Holmakefile U hol98/help/src/Htmlsigs.sig U hol98/help/src/Htmlsigs.sml U hol98/help/src/Keepers.sml U hol98/help/src/Lexer.lex U hol98/help/src/Makefile U hol98/help/src/Makefile.w32 U hol98/help/src/Parser.grm U hol98/help/src/Parsspec.sml U hol98/help/src/Printbase.sml U hol98/help/src/README U hol98/help/src/Stack.sig U hol98/help/src/Stack.sml U hol98/help/src/Texsigs.sig U hol98/help/src/Texsigs.sml U hol98/help/src/index.html cvs server: Updating hol98/sigobj U hol98/sigobj/README cvs server: Updating hol98/src cvs server: Updating hol98/src/0 U hol98/src/0/.cvsignore U hol98/src/0/Count.sig U hol98/src/0/Count.sml U hol98/src/0/Definition-sig.sml U hol98/src/0/Definition.sml U hol98/src/0/Feedback.sig U hol98/src/0/Feedback.sml U hol98/src/0/Globals.sig U hol98/src/0/HOLset.sig U hol98/src/0/HOLset.sml U hol98/src/0/HolKernel.sml U hol98/src/0/Holmakefile U hol98/src/0/KernelTypes.sig U hol98/src/0/KernelTypes.sml U hol98/src/0/Lexis.sig U hol98/src/0/Lexis.sml U hol98/src/0/Lib.sig U hol98/src/0/Lib.sml U hol98/src/0/Net-sig.sml U hol98/src/0/Net.sml U hol98/src/0/Overlay.sml U hol98/src/0/Raw-sig.sml U hol98/src/0/Sig.sml U hol98/src/0/Subst.sig U hol98/src/0/Subst.sml U hol98/src/0/Tag-sig.sml U hol98/src/0/Tag.sml U hol98/src/0/Term-sig.sml U hol98/src/0/Term.sml U hol98/src/0/Theory-sig.sml U hol98/src/0/Theory.sml U hol98/src/0/TheoryPP-sig.sml U hol98/src/0/TheoryPP.sml U hol98/src/0/Thm-sig.sml U hol98/src/0/Thm.sml U hol98/src/0/Type-sig.sml U hol98/src/0/Type.sml cvs server: Updating hol98/src/BoyerMoore U hol98/src/BoyerMoore/BoyerMooreClausalForm.sml U hol98/src/BoyerMoore/BoyerMooreDefinitions.sml U hol98/src/BoyerMoore/BoyerMooreEnvironment.sml U hol98/src/BoyerMoore/BoyerMooreEqualities.sml U hol98/src/BoyerMoore/BoyerMooreGeneralize.sml U hol98/src/BoyerMoore/BoyerMooreInduction.sml U hol98/src/BoyerMoore/BoyerMooreIrrelevance.sml U hol98/src/BoyerMoore/BoyerMooreLib.sml U hol98/src/BoyerMoore/BoyerMooreRewriteRules.sml U hol98/src/BoyerMoore/BoyerMooreShells.sml U hol98/src/BoyerMoore/BoyerMooreStructEqual.sml U hol98/src/BoyerMoore/BoyerMooreSupport.sml U hol98/src/BoyerMoore/BoyerMooreTermsAndClauses.sml U hol98/src/BoyerMoore/BoyerMooreWaterfall.sml U hol98/src/BoyerMoore/READ-ME cvs server: Updating hol98/src/HolBdd U hol98/src/HolBdd/HolBdd.sig U hol98/src/HolBdd/HolBdd.sml U hol98/src/HolBdd/HolBddLib.sml U hol98/src/HolBdd/HolBddPaper.ps U hol98/src/HolBdd/HolBddScript.sml U hol98/src/HolBdd/StateEnum.sig U hol98/src/HolBdd/StateEnum.sml cvs server: Updating hol98/src/IndDef U hol98/src/IndDef/IndDefLib.sig U hol98/src/IndDef/IndDefLib.sml U hol98/src/IndDef/IndDefRules.sig U hol98/src/IndDef/IndDefRules.sml U hol98/src/IndDef/InductiveDefinition.sig U hol98/src/IndDef/InductiveDefinition.sml U hol98/src/IndDef/READ-ME cvs server: Updating hol98/src/arith cvs server: Updating hol98/src/arith/Manual cvs server: Updating hol98/src/arith/help cvs server: Updating hol98/src/arith/help/entries cvs server: Updating hol98/src/arith/src cvs server: Updating hol98/src/bag U hol98/src/bag/bagLib.sig U hol98/src/bag/bagLib.sml U hol98/src/bag/bagScript.sml U hol98/src/bag/bagSimps.sig U hol98/src/bag/bagSimps.sml U hol98/src/bag/bagSyntax.sig U hol98/src/bag/bagSyntax.sml U hol98/src/bag/containerScript.sml U hol98/src/bag/mnUtils.sml cvs server: Updating hol98/src/basicHol90 cvs server: Updating hol98/src/basicProof U hol98/src/basicProof/BasicProvers.sig U hol98/src/basicProof/BasicProvers.sml cvs server: Updating hol98/src/bool U hol98/src/bool/.cvsignore U hol98/src/bool/Abbrev.sig U hol98/src/bool/Abbrev.sml U hol98/src/bool/Conv.sig U hol98/src/bool/Conv.sml U hol98/src/bool/DB.sig U hol98/src/bool/DB.sml U hol98/src/bool/DefnBase.sig U hol98/src/bool/DefnBase.sml U hol98/src/bool/Drule.sig U hol98/src/bool/Drule.sml U hol98/src/bool/Ho_Net.sig U hol98/src/bool/Ho_Net.sml U hol98/src/bool/Ho_Rewrite.sig U hol98/src/bool/Ho_Rewrite.sml U hol98/src/bool/Pmatch.sig U hol98/src/bool/Pmatch.sml U hol98/src/bool/Prim_rec.sig U hol98/src/bool/Prim_rec.sml U hol98/src/bool/Psyntax.sig U hol98/src/bool/Psyntax.sml U hol98/src/bool/QConv.sig U hol98/src/bool/QConv.sml U hol98/src/bool/Rewrite.sig U hol98/src/bool/Rewrite.sml U hol98/src/bool/Rsyntax.sig U hol98/src/bool/Rsyntax.sml U hol98/src/bool/Tactic.sig U hol98/src/bool/Tactic.sml U hol98/src/bool/Tactical.sig U hol98/src/bool/Tactical.sml U hol98/src/bool/Thm_cont.sig U hol98/src/bool/Thm_cont.sml U hol98/src/bool/TypeBase.sig U hol98/src/bool/TypeBase.sml U hol98/src/bool/TypeBasePure.sig U hol98/src/bool/TypeBasePure.sml U hol98/src/bool/boolLib.sml U hol98/src/bool/boolScript.sml U hol98/src/bool/boolSyntax.sig U hol98/src/bool/boolSyntax.sml U hol98/src/bool/fastbuild.sml U hol98/src/bool/holmakebuild.sml cvs server: Updating hol98/src/boss U hol98/src/boss/SingleStep.sig U hol98/src/boss/SingleStep.sml U hol98/src/boss/bossLib.sig U hol98/src/boss/bossLib.sml cvs server: Updating hol98/src/combin U hol98/src/combin/combinScript.sml cvs server: Updating hol98/src/compute cvs server: Updating hol98/src/compute/Manual U hol98/src/compute/Manual/description.tex cvs server: Updating hol98/src/compute/examples U hol98/src/compute/examples/Arith.sml U hol98/src/compute/examples/MergeSort.sml U hol98/src/compute/examples/Sort.sml cvs server: Updating hol98/src/compute/help cvs server: Updating hol98/src/compute/help/entries cvs server: Updating hol98/src/compute/src U hol98/src/compute/src/clauses.sml U hol98/src/compute/src/computeLib.sig U hol98/src/compute/src/computeLib.sml U hol98/src/compute/src/compute_rules.sig U hol98/src/compute/src/compute_rules.sml U hol98/src/compute/src/equations.sml cvs server: Updating hol98/src/datatype U hol98/src/datatype/Datatype.sig U hol98/src/datatype/Datatype.sml U hol98/src/datatype/EnumType.sig U hol98/src/datatype/EnumType.sml U hol98/src/datatype/Mutual.sig U hol98/src/datatype/Mutual.sml U hol98/src/datatype/ind_typeScript.sml U hol98/src/datatype/ind_types.sig U hol98/src/datatype/ind_types.sml U hol98/src/datatype/jrh.test U hol98/src/datatype/ph.test cvs server: Updating hol98/src/datatype/basicrec U hol98/src/datatype/basicrec/Define_type.sig U hol98/src/datatype/basicrec/Define_type.sml U hol98/src/datatype/basicrec/Define_type.sml.0 U hol98/src/datatype/basicrec/rec_typeScript.sml cvs server: Updating hol98/src/datatype/equiv U hol98/src/datatype/equiv/EquivType.sig U hol98/src/datatype/equiv/EquivType.sml cvs server: Updating hol98/src/datatype/mutrec U hol98/src/datatype/mutrec/ConsThms.sig U hol98/src/datatype/mutrec/ConsThms.sml U hol98/src/datatype/mutrec/MutRecDef.sig U hol98/src/datatype/mutrec/MutRecDef.sml U hol98/src/datatype/mutrec/MutRecMask.sig U hol98/src/datatype/mutrec/MutRecMask.sml U hol98/src/datatype/mutrec/Recftn.sig U hol98/src/datatype/mutrec/Recftn.sml U hol98/src/datatype/mutrec/TypeInfo.sig U hol98/src/datatype/mutrec/TypeInfo.sml U hol98/src/datatype/mutrec/mutrecLib.sig U hol98/src/datatype/mutrec/mutrecLib.sml cvs server: Updating hol98/src/datatype/mutrec/examples U hol98/src/datatype/mutrec/examples/example.sml U hol98/src/datatype/mutrec/examples/test.sml U hol98/src/datatype/mutrec/examples/var_example.sml U hol98/src/datatype/mutrec/examples/var_example2.sml cvs server: Updating hol98/src/datatype/mutrec/utils U hol98/src/datatype/mutrec/utils/elsaUtils.sig U hol98/src/datatype/mutrec/utils/elsaUtils.sml cvs server: Updating hol98/src/datatype/mutual U hol98/src/datatype/mutual/Def_MN_Func.sig U hol98/src/datatype/mutual/Def_MN_Func.sml U hol98/src/datatype/mutual/Def_MN_Type.sig U hol98/src/datatype/mutual/Def_MN_Type.sml U hol98/src/datatype/mutual/MutualIndThen.sig U hol98/src/datatype/mutual/MutualIndThen.sml U hol98/src/datatype/mutual/mutualLib.sig U hol98/src/datatype/mutual/mutualLib.sml cvs server: Updating hol98/src/datatype/mutual/examples U hol98/src/datatype/mutual/examples/assertion.sml U hol98/src/datatype/mutual/examples/pat.sml U hol98/src/datatype/mutual/examples/rectypes.ml U hol98/src/datatype/mutual/examples/rectypes.sml U hol98/src/datatype/mutual/examples/rectypes.sml.0 U hol98/src/datatype/mutual/examples/smallML.sml U hol98/src/datatype/mutual/examples/test.sml cvs server: Updating hol98/src/datatype/mutual/src U hol98/src/datatype/mutual/src/define_mutual_types.sig U hol98/src/datatype/mutual/src/define_mutual_types.sml U hol98/src/datatype/mutual/src/load_nested_rec_lib.sml U hol98/src/datatype/mutual/src/makefile U hol98/src/datatype/mutual/src/mk_mutual_lib.sml U hol98/src/datatype/mutual/src/mutrec.yak U hol98/src/datatype/mutual/src/mutualLib.sml U hol98/src/datatype/mutual/src/mutual_induct_then.sig U hol98/src/datatype/mutual/src/mutual_induct_then.sml U hol98/src/datatype/mutual/src/recftn.sml cvs server: Updating hol98/src/datatype/nestrec U hol98/src/datatype/nestrec/DefType.sig U hol98/src/datatype/nestrec/DefType.sml U hol98/src/datatype/nestrec/DefTypeInfo.sig U hol98/src/datatype/nestrec/DefTypeInfo.sml U hol98/src/datatype/nestrec/ExistsFuns.sig U hol98/src/datatype/nestrec/ExistsFuns.sml U hol98/src/datatype/nestrec/GenFuns.sig U hol98/src/datatype/nestrec/GenFuns.sml U hol98/src/datatype/nestrec/NestedRecMask.sig U hol98/src/datatype/nestrec/NestedRecMask.sml U hol98/src/datatype/nestrec/StringTable.sig U hol98/src/datatype/nestrec/StringTable.sml U hol98/src/datatype/nestrec/TypeOpTable.sig U hol98/src/datatype/nestrec/TypeOpTable.sml U hol98/src/datatype/nestrec/TypeTable.sig U hol98/src/datatype/nestrec/TypeTable.sml U hol98/src/datatype/nestrec/nested_recLib.sig U hol98/src/datatype/nestrec/nested_recLib.sml cvs server: Updating hol98/src/datatype/nestrec/examples U hol98/src/datatype/nestrec/examples/e1.sml U hol98/src/datatype/nestrec/examples/tmp.sml U hol98/src/datatype/nestrec/examples/tv.sml cvs server: Updating hol98/src/datatype/parse U hol98/src/datatype/parse/ParseDatatype.sig U hol98/src/datatype/parse/ParseDatatype.sml cvs server: Updating hol98/src/datatype/record U hol98/src/datatype/record/RecordType.sig U hol98/src/datatype/record/RecordType.sml cvs server: Updating hol98/src/decision U hol98/src/decision/READ-ME U hol98/src/decision/examples.sml cvs server: Updating hol98/src/decision/src U hol98/src/decision/src/.cvsignore U hol98/src/decision/src/CongruenceClosure.sml U hol98/src/decision/src/CongruenceClosurePairs.sml U hol98/src/decision/src/CongruenceClosureTypes.sml U hol98/src/decision/src/Decide.sml U hol98/src/decision/src/DecideNum.sml U hol98/src/decision/src/DecidePair.sml U hol98/src/decision/src/DecideProp.sml U hol98/src/decision/src/DecideTypes.sml U hol98/src/decision/src/DecideUninterp.sml U hol98/src/decision/src/DecisionArithConvs.sig U hol98/src/decision/src/DecisionArithConvs.sml U hol98/src/decision/src/DecisionConv.sig U hol98/src/decision/src/DecisionConv.sml U hol98/src/decision/src/DecisionNormConvs.sml U hol98/src/decision/src/DecisionSupport.sml U hol98/src/decision/src/DecisionTheorems.sig U hol98/src/decision/src/DecisionTheorems.sml U hol98/src/decision/src/HOLTypeInfo.sml U hol98/src/decision/src/LazyRules.sml U hol98/src/decision/src/LazyThm.sig U hol98/src/decision/src/LazyThm.sml U hol98/src/decision/src/NormalizeBool.sml U hol98/src/decision/src/NumArith.sig U hol98/src/decision/src/NumArith.sml U hol98/src/decision/src/NumArithCons.sig U hol98/src/decision/src/NumArithCons.sml U hol98/src/decision/src/NumHOLType.sig U hol98/src/decision/src/NumHOLType.sml U hol98/src/decision/src/NumInequalityCoeffs.sig U hol98/src/decision/src/NumInequalityCoeffs.sml U hol98/src/decision/src/NumType.sig U hol98/src/decision/src/NumType.sml U hol98/src/decision/src/Taut.sig U hol98/src/decision/src/Taut.sml U hol98/src/decision/src/decisionLib.sml cvs server: Updating hol98/src/finite_map U hol98/src/finite_map/finite_mapScript.sml cvs server: Updating hol98/src/goalstack U hol98/src/goalstack/Bwd.sig U hol98/src/goalstack/Bwd.sml U hol98/src/goalstack/GoalstackPure.sig U hol98/src/goalstack/GoalstackPure.sml U hol98/src/goalstack/History.sig U hol98/src/goalstack/History.sml U hol98/src/goalstack/goalstackLib.sig U hol98/src/goalstack/goalstackLib.sml cvs server: Updating hol98/src/ho_match cvs server: Updating hol98/src/hol88 U hol98/src/hol88/hol88Lib.sig U hol98/src/hol88/hol88Lib.sml cvs server: Updating hol98/src/hol88/help cvs server: Updating hol98/src/hol88/help/entries U hol98/src/hol88/help/entries/CB.doc U hol98/src/hol88/help/entries/Co.doc U hol98/src/hol88/help/entries/Compat.doc U hol98/src/hol88/help/entries/GEN_ALL.doc U hol98/src/hol88/help/entries/KI.doc U hol98/src/hol88/help/entries/PROVE.doc U hol98/src/hol88/help/entries/W.doc U hol98/src/hol88/help/entries/assoc.doc U hol98/src/hol88/help/entries/butlast.doc U hol98/src/hol88/help/entries/conjuncts.doc U hol98/src/hol88/help/entries/disjuncts.doc U hol98/src/hol88/help/entries/find.doc U hol98/src/hol88/help/entries/flat.doc U hol98/src/hol88/help/entries/forall.doc U hol98/src/hol88/help/entries/frees.doc U hol98/src/hol88/help/entries/freesl.doc U hol98/src/hol88/help/entries/funpow.doc U hol98/src/hol88/help/entries/inst_type-lc.doc U hol98/src/hol88/help/entries/int_of_string.doc U hol98/src/hol88/help/entries/last.doc U hol98/src/hol88/help/entries/match.doc U hol98/src/hol88/help/entries/new_axiom.doc U hol98/src/hol88/help/entries/new_infix_prim_rec_definition.doc U hol98/src/hol88/help/entries/new_prim_rec_definition.doc U hol98/src/hol88/help/entries/oo.doc U hol98/src/hol88/help/entries/prove_thm.doc U hol98/src/hol88/help/entries/replicate.doc U hol98/src/hol88/help/entries/rev_assoc.doc U hol98/src/hol88/help/entries/save.doc U hol98/src/hol88/help/entries/setify.doc U hol98/src/hol88/help/entries/string_of_int.doc U hol98/src/hol88/help/entries/tyvars.doc U hol98/src/hol88/help/entries/tyvarsl.doc cvs server: Updating hol98/src/hol90 U hol98/src/hol90/HOLScript.sml U hol98/src/hol90/HOLSimps.sig U hol98/src/hol90/HOLSimps.sml U hol98/src/hol90/hol90Lib.sml cvs server: Updating hol98/src/ind_def U hol98/src/ind_def/READ-ME cvs server: Updating hol98/src/ind_def/Manual U hol98/src/ind_def/Manual/READ-ME U hol98/src/ind_def/Manual/alltt.sty U hol98/src/ind_def/Manual/layout.sty U hol98/src/ind_def/Manual/macros.tex U hol98/src/ind_def/Manual/paper.tex cvs server: Updating hol98/src/ind_def/examples U hol98/src/ind_def/examples/algebraScript.sml U hol98/src/ind_def/examples/clScript.sml U hol98/src/ind_def/examples/milScript.sml U hol98/src/ind_def/examples/opsemScript.sml cvs server: Updating hol98/src/ind_def/src U hol98/src/ind_def/src/ind_defLib.sig U hol98/src/ind_def/src/ind_defLib.sml cvs server: Updating hol98/src/integer U hol98/src/integer/Cooper.sig U hol98/src/integer/Cooper.sml U hol98/src/integer/CooperMath.sig U hol98/src/integer/CooperMath.sml U hol98/src/integer/CooperSyntax.sig U hol98/src/integer/CooperSyntax.sml U hol98/src/integer/CooperThms.sml U hol98/src/integer/dividesScript.sml U hol98/src/integer/gcdScript.sml U hol98/src/integer/intLib.sig U hol98/src/integer/intLib.sml U hol98/src/integer/intSimps.sig U hol98/src/integer/intSimps.sml U hol98/src/integer/intSyntax.sig U hol98/src/integer/intSyntax.sml U hol98/src/integer/int_arithScript.sml U hol98/src/integer/integerScript.sml U hol98/src/integer/jrhUtils.sig U hol98/src/integer/jrhUtils.sml U hol98/src/integer/primeScript.sml cvs server: Updating hol98/src/integer/testing U hol98/src/integer/testing/Holmakefile U hol98/src/integer/testing/gen_bc_problem.sml U hol98/src/integer/testing/genproblem.sml U hol98/src/integer/testing/number.sh U hol98/src/integer/testing/readproblemfile.sig U hol98/src/integer/testing/readproblemfile.sml U hol98/src/integer/testing/tcooper.c U hol98/src/integer/testing/test_coopers.sml U hol98/src/integer/testing/testdp.sml cvs server: Updating hol98/src/list U hol98/src/list/README cvs server: Updating hol98/src/list/examples U hol98/src/list/examples/test.sml cvs server: Updating hol98/src/list/help cvs server: Updating hol98/src/list/help/entries U hol98/src/list/help/entries/ALL_EL_CONV.doc U hol98/src/list/help/entries/AND_EL_CONV.doc U hol98/src/list/help/entries/APPEND_CONV.doc U hol98/src/list/help/entries/BUTFIRSTN_CONV.doc U hol98/src/list/help/entries/BUTLASTN_CONV.doc U hol98/src/list/help/entries/BUTLAST_CONV.doc U hol98/src/list/help/entries/ELL_CONV.doc U hol98/src/list/help/entries/EL_CONV.doc U hol98/src/list/help/entries/EQ_LENGTH_INDUCT_TAC.doc U hol98/src/list/help/entries/EQ_LENGTH_SNOC_INDUCT_TAC.doc U hol98/src/list/help/entries/FILTER_CONV.doc U hol98/src/list/help/entries/FIRSTN_CONV.doc U hol98/src/list/help/entries/FLAT_CONV.doc U hol98/src/list/help/entries/FOLDL_CONV.doc U hol98/src/list/help/entries/FOLDR_CONV.doc U hol98/src/list/help/entries/GENLIST_CONV.doc U hol98/src/list/help/entries/IS_EL_CONV.doc U hol98/src/list/help/entries/LASTN_CONV.doc U hol98/src/list/help/entries/LAST_CONV.doc U hol98/src/list/help/entries/LENGTH_CONV.doc U hol98/src/list/help/entries/LIST_CONV.doc U hol98/src/list/help/entries/LIST_INDUCT_TAC.doc U hol98/src/list/help/entries/MAP2_CONV.doc U hol98/src/list/help/entries/MAP_CONV.doc U hol98/src/list/help/entries/OR_EL_CONV.doc U hol98/src/list/help/entries/PURE_LIST_CONV.doc U hol98/src/list/help/entries/REPLICATE.doc U hol98/src/list/help/entries/REPLICATE_CONV.doc U hol98/src/list/help/entries/REVERSE_CONV.doc U hol98/src/list/help/entries/SCANL_CONV.doc U hol98/src/list/help/entries/SCANR_CONV.doc U hol98/src/list/help/entries/SEG_CONV.doc U hol98/src/list/help/entries/SNOC_CONV.doc U hol98/src/list/help/entries/SNOC_INDUCT_TAC.doc U hol98/src/list/help/entries/SOME_EL_CONV.doc U hol98/src/list/help/entries/SUM_CONV.doc U hol98/src/list/help/entries/X_LIST_CONV.doc U hol98/src/list/help/entries/list_FOLD_CONV.doc U hol98/src/list/help/entries/list_thm_database.doc U hol98/src/list/help/entries/set_list_thm_database.doc cvs server: Updating hol98/src/list/src U hol98/src/list/src/ListConv1.sig U hol98/src/list/src/ListConv1.sml U hol98/src/list/src/listLib.sig U hol98/src/list/src/listLib.sml U hol98/src/list/src/listScript.sml U hol98/src/list/src/listSimps.sig U hol98/src/list/src/listSimps.sml U hol98/src/list/src/listSyntax.sig U hol98/src/list/src/listSyntax.sml U hol98/src/list/src/operatorScript.sml U hol98/src/list/src/rich_listScript.sml U hol98/src/list/src/rich_listSimps.sig U hol98/src/list/src/rich_listSimps.sml cvs server: Updating hol98/src/lite U hol98/src/lite/liteLib.sig U hol98/src/lite/liteLib.sml cvs server: Updating hol98/src/lite/old cvs server: Updating hol98/src/llist U hol98/src/llist/llistScript.sml cvs server: Updating hol98/src/meson U hol98/src/meson/READ-ME U hol98/src/meson/test.sml cvs server: Updating hol98/src/meson/src U hol98/src/meson/src/Canon_Port.sig U hol98/src/meson/src/Canon_Port.sml U hol98/src/meson/src/jrhTactics.sig U hol98/src/meson/src/jrhTactics.sml U hol98/src/meson/src/mesonLib.sig U hol98/src/meson/src/mesonLib.sml U hol98/src/meson/src/mesonLib.sml.0 cvs server: Updating hol98/src/muddy U hol98/src/muddy/MuddyCore.sml U hol98/src/muddy/bdd.sig U hol98/src/muddy/bdd.sml U hol98/src/muddy/bvec.sig U hol98/src/muddy/bvec.sml U hol98/src/muddy/fdd.sig U hol98/src/muddy/fdd.sml U hol98/src/muddy/muddyLib.sig U hol98/src/muddy/muddyLib.sml cvs server: Updating hol98/src/muddy/buddy17 cvs server: Updating hol98/src/muddy/buddy17/doc cvs server: Updating hol98/src/muddy/buddy17/examples cvs server: Updating hol98/src/muddy/buddy17/examples/adder cvs server: Updating hol98/src/muddy/buddy17/examples/calculator cvs server: Updating hol98/src/muddy/buddy17/examples/cmilner cvs server: Updating hol98/src/muddy/buddy17/examples/fdd cvs server: Updating hol98/src/muddy/buddy17/examples/milner cvs server: Updating hol98/src/muddy/buddy17/examples/queen cvs server: Updating hol98/src/muddy/buddy17/src cvs server: Updating hol98/src/muddy/muddyC U hol98/src/muddy/muddyC/muddy.c cvs server: Updating hol98/src/muddy/muddyC/buddy17 U hol98/src/muddy/muddyC/buddy17/makefile cvs server: Updating hol98/src/muddy/muddyC/buddy17/doc U hol98/src/muddy/muddyC/buddy17/doc/bddnotes.ps U hol98/src/muddy/muddyC/buddy17/doc/buddy.ps U hol98/src/muddy/muddyC/buddy17/doc/makefile U hol98/src/muddy/muddyC/buddy17/doc/tech.txt cvs server: Updating hol98/src/muddy/muddyC/buddy17/examples cvs server: Updating hol98/src/muddy/muddyC/buddy17/src U hol98/src/muddy/muddyC/buddy17/src/bdd.h U hol98/src/muddy/muddyC/buddy17/src/bddio.c U hol98/src/muddy/muddyC/buddy17/src/bddop.c U hol98/src/muddy/muddyC/buddy17/src/bddtree.h U hol98/src/muddy/muddyC/buddy17/src/bvec.c U hol98/src/muddy/muddyC/buddy17/src/bvec.h U hol98/src/muddy/muddyC/buddy17/src/cache.c U hol98/src/muddy/muddyC/buddy17/src/cache.h U hol98/src/muddy/muddyC/buddy17/src/cppext.cxx U hol98/src/muddy/muddyC/buddy17/src/depend.inf U hol98/src/muddy/muddyC/buddy17/src/fdd.c U hol98/src/muddy/muddyC/buddy17/src/fdd.h U hol98/src/muddy/muddyC/buddy17/src/kernel.c U hol98/src/muddy/muddyC/buddy17/src/kernel.h U hol98/src/muddy/muddyC/buddy17/src/makefile U hol98/src/muddy/muddyC/buddy17/src/pairs.c U hol98/src/muddy/muddyC/buddy17/src/reorder.c U hol98/src/muddy/muddyC/buddy17/src/tree.c cvs server: Updating hol98/src/num U hol98/src/num/NonRecSize.sml U hol98/src/num/numLib.sig U hol98/src/num/numLib.sml cvs server: Updating hol98/src/num/arith cvs server: Updating hol98/src/num/arith/Manual U hol98/src/num/arith/Manual/Makefile U hol98/src/num/arith/Manual/arith.tex U hol98/src/num/arith/Manual/description.tex U hol98/src/num/arith/Manual/entries-intro.tex U hol98/src/num/arith/Manual/entries.tex U hol98/src/num/arith/Manual/references.tex U hol98/src/num/arith/Manual/title.tex cvs server: Updating hol98/src/num/arith/help cvs server: Updating hol98/src/num/arith/help/entries U hol98/src/num/arith/help/entries/ARITH_CONV.doc U hol98/src/num/arith/help/entries/ARITH_FORM_NORM_CONV.doc U hol98/src/num/arith/help/entries/COND_ELIM_CONV.doc U hol98/src/num/arith/help/entries/DISJ_INEQS_FALSE_CONV.doc U hol98/src/num/arith/help/entries/EXISTS_ARITH_CONV.doc U hol98/src/num/arith/help/entries/FORALL_ARITH_CONV.doc U hol98/src/num/arith/help/entries/INSTANCE_T_CONV.doc U hol98/src/num/arith/help/entries/NEGATE_CONV.doc U hol98/src/num/arith/help/entries/PRENEX_CONV.doc U hol98/src/num/arith/help/entries/SUB_AND_COND_ELIM_CONV.doc U hol98/src/num/arith/help/entries/is_prenex.doc U hol98/src/num/arith/help/entries/is_presburger.doc U hol98/src/num/arith/help/entries/non_presburger_subterms.doc cvs server: Updating hol98/src/num/arith/src U hol98/src/num/arith/src/.cvsignore U hol98/src/num/arith/src/Arith.sig U hol98/src/num/arith/src/Arith.sml U hol98/src/num/arith/src/Arith_cons.sig U hol98/src/num/arith/src/Arith_cons.sml U hol98/src/num/arith/src/Exists_arith.sig U hol98/src/num/arith/src/Exists_arith.sml U hol98/src/num/arith/src/Gen_arith.sig U hol98/src/num/arith/src/Gen_arith.sml U hol98/src/num/arith/src/Instance.sig U hol98/src/num/arith/src/Instance.sml U hol98/src/num/arith/src/Int_extra.sig U hol98/src/num/arith/src/Int_extra.sml U hol98/src/num/arith/src/Norm_arith.sig U hol98/src/num/arith/src/Norm_arith.sml U hol98/src/num/arith/src/Norm_bool.sig U hol98/src/num/arith/src/Norm_bool.sml U hol98/src/num/arith/src/Norm_ineqs.sig U hol98/src/num/arith/src/Norm_ineqs.sml U hol98/src/num/arith/src/Prenex.sig U hol98/src/num/arith/src/Prenex.sml U hol98/src/num/arith/src/Qconv.sig U hol98/src/num/arith/src/Qconv.sml U hol98/src/num/arith/src/Rationals.sig U hol98/src/num/arith/src/Rationals.sml U hol98/src/num/arith/src/Sol_ranges.sig U hol98/src/num/arith/src/Sol_ranges.sml U hol98/src/num/arith/src/Solve.sig U hol98/src/num/arith/src/Solve.sml U hol98/src/num/arith/src/Solve_ineqs.sig U hol98/src/num/arith/src/Solve_ineqs.sml U hol98/src/num/arith/src/Streams.sig U hol98/src/num/arith/src/Streams.sml U hol98/src/num/arith/src/Sub_and_cond.sig U hol98/src/num/arith/src/Sub_and_cond.sml U hol98/src/num/arith/src/Sup_Inf.sig U hol98/src/num/arith/src/Sup_Inf.sml U hol98/src/num/arith/src/Term_coeffs.sig U hol98/src/num/arith/src/Term_coeffs.sml U hol98/src/num/arith/src/Theorems.sig U hol98/src/num/arith/src/Theorems.sml U hol98/src/num/arith/src/Thm_convs.sig U hol98/src/num/arith/src/Thm_convs.sml U hol98/src/num/arith/src/numSimps.sig U hol98/src/num/arith/src/numSimps.sml cvs server: Updating hol98/src/num/reduce cvs server: Updating hol98/src/num/reduce/Manual U hol98/src/num/reduce/Manual/Makefile U hol98/src/num/reduce/Manual/description.tex U hol98/src/num/reduce/Manual/entries-intro.tex U hol98/src/num/reduce/Manual/index.tex U hol98/src/num/reduce/Manual/reduce.tex U hol98/src/num/reduce/Manual/title.tex cvs server: Updating hol98/src/num/reduce/help cvs server: Updating hol98/src/num/reduce/help/entries U hol98/src/num/reduce/help/entries/ADD_CONV.doc U hol98/src/num/reduce/help/entries/AND_CONV.doc U hol98/src/num/reduce/help/entries/BEQ_CONV.doc U hol98/src/num/reduce/help/entries/COND_CONV.doc U hol98/src/num/reduce/help/entries/DIV_CONV.doc U hol98/src/num/reduce/help/entries/EXP_CONV.doc U hol98/src/num/reduce/help/entries/GE_CONV.doc U hol98/src/num/reduce/help/entries/GT_CONV.doc U hol98/src/num/reduce/help/entries/IMP_CONV.doc U hol98/src/num/reduce/help/entries/LE_CONV.doc U hol98/src/num/reduce/help/entries/LT_CONV.doc U hol98/src/num/reduce/help/entries/MOD_CONV.doc U hol98/src/num/reduce/help/entries/MUL_CONV.doc U hol98/src/num/reduce/help/entries/NEQ_CONV.doc U hol98/src/num/reduce/help/entries/NOT_CONV.doc U hol98/src/num/reduce/help/entries/OR_CONV.doc U hol98/src/num/reduce/help/entries/PRE_CONV.doc U hol98/src/num/reduce/help/entries/REDUCE_CONV.doc U hol98/src/num/reduce/help/entries/REDUCE_RULE.doc U hol98/src/num/reduce/help/entries/REDUCE_TAC.doc U hol98/src/num/reduce/help/entries/RED_CONV.doc U hol98/src/num/reduce/help/entries/SBC_CONV.doc U hol98/src/num/reduce/help/entries/SUC_CONV.doc cvs server: Updating hol98/src/num/reduce/src U hol98/src/num/reduce/src/Arithconv.sig U hol98/src/num/reduce/src/Arithconv.sml U hol98/src/num/reduce/src/Boolconv.sig U hol98/src/num/reduce/src/Boolconv.sml U hol98/src/num/reduce/src/reduceLib.sig U hol98/src/num/reduce/src/reduceLib.sml cvs server: Updating hol98/src/num/theories U hol98/src/num/theories/Num_conv.sig U hol98/src/num/theories/Num_conv.sml U hol98/src/num/theories/arithmeticScript.sml U hol98/src/num/theories/numScript.sml U hol98/src/num/theories/numSyntax.sig U hol98/src/num/theories/numSyntax.sml U hol98/src/num/theories/numeralScript.sml U hol98/src/num/theories/prim_recScript.sml cvs server: Updating hol98/src/one U hol98/src/one/oneScript.sml cvs server: Updating hol98/src/option U hol98/src/option/READ-ME U hol98/src/option/optionLib.sig U hol98/src/option/optionLib.sml U hol98/src/option/optionScript.sml U hol98/src/option/optionSimps.sig U hol98/src/option/optionSimps.sml U hol98/src/option/optionSyntax.sig U hol98/src/option/optionSyntax.sml cvs server: Updating hol98/src/pair U hol98/src/pair/COPYRIGHT cvs server: Updating hol98/src/pair/Manual U hol98/src/pair/Manual/Makefile U hol98/src/pair/Manual/description.tex U hol98/src/pair/Manual/entries-intro.tex U hol98/src/pair/Manual/index.tex U hol98/src/pair/Manual/pair.tex U hol98/src/pair/Manual/theorems-intro.tex U hol98/src/pair/Manual/title.tex cvs server: Updating hol98/src/pair/help cvs server: Updating hol98/src/pair/help/entries U hol98/src/pair/help/entries/AND_PEXISTS_CONV.doc U hol98/src/pair/help/entries/AND_PFORALL_CONV.doc U hol98/src/pair/help/entries/CURRY_CONV.doc U hol98/src/pair/help/entries/CURRY_EXISTS_CONV.doc U hol98/src/pair/help/entries/CURRY_FORALL_CONV.doc U hol98/src/pair/help/entries/FILTER_PGEN_TAC.doc U hol98/src/pair/help/entries/FILTER_PSTRIP_TAC.doc U hol98/src/pair/help/entries/FILTER_PSTRIP_THEN.doc U hol98/src/pair/help/entries/GEN_PALPHA_CONV.doc U hol98/src/pair/help/entries/GPSPEC.doc U hol98/src/pair/help/entries/HALF_MK_PABS.doc U hol98/src/pair/help/entries/IPSPEC.doc U hol98/src/pair/help/entries/IPSPECL.doc U hol98/src/pair/help/entries/LEFT_AND_PEXISTS_CONV.doc U hol98/src/pair/help/entries/LEFT_AND_PFORALL_CONV.doc U hol98/src/pair/help/entries/LEFT_IMP_PEXISTS_CONV.doc U hol98/src/pair/help/entries/LEFT_IMP_PFORALL_CONV.doc U hol98/src/pair/help/entries/LEFT_LIST_PBETA.doc U hol98/src/pair/help/entries/LEFT_OR_PEXISTS_CONV.doc U hol98/src/pair/help/entries/LEFT_OR_PFORALL_CONV.doc U hol98/src/pair/help/entries/LEFT_PBETA.doc U hol98/src/pair/help/entries/LIST_MK_PEXISTS.doc U hol98/src/pair/help/entries/LIST_MK_PFORALL.doc U hol98/src/pair/help/entries/LIST_PBETA_CONV.doc U hol98/src/pair/help/entries/MK_PABS.doc U hol98/src/pair/help/entries/MK_PAIR.doc U hol98/src/pair/help/entries/MK_PEXISTS.doc U hol98/src/pair/help/entries/MK_PFORALL.doc U hol98/src/pair/help/entries/MK_PSELECT.doc U hol98/src/pair/help/entries/NOT_PEXISTS_CONV.doc U hol98/src/pair/help/entries/NOT_PFORALL_CONV.doc U hol98/src/pair/help/entries/OR_PEXISTS_CONV.doc U hol98/src/pair/help/entries/OR_PFORALL_CONV.doc U hol98/src/pair/help/entries/PABS.doc U hol98/src/pair/help/entries/PABS_CONV.doc U hol98/src/pair/help/entries/PAIR_CONV.doc U hol98/src/pair/help/entries/PALPHA.doc U hol98/src/pair/help/entries/PALPHA_CONV.doc U hol98/src/pair/help/entries/PART_PMATCH.doc U hol98/src/pair/help/entries/PBETA_CONV.doc U hol98/src/pair/help/entries/PBETA_RULE.doc U hol98/src/pair/help/entries/PBETA_TAC.doc U hol98/src/pair/help/entries/PCHOOSE.doc U hol98/src/pair/help/entries/PCHOOSE_TAC.doc U hol98/src/pair/help/entries/PCHOOSE_THEN.doc U hol98/src/pair/help/entries/PETA_CONV.doc U hol98/src/pair/help/entries/PEXISTENCE.doc U hol98/src/pair/help/entries/PEXISTS.doc U hol98/src/pair/help/entries/PEXISTS_AND_CONV.doc U hol98/src/pair/help/entries/PEXISTS_CONV.doc U hol98/src/pair/help/entries/PEXISTS_EQ.doc U hol98/src/pair/help/entries/PEXISTS_IMP.doc U hol98/src/pair/help/entries/PEXISTS_IMP_CONV.doc U hol98/src/pair/help/entries/PEXISTS_NOT_CONV.doc U hol98/src/pair/help/entries/PEXISTS_OR_CONV.doc U hol98/src/pair/help/entries/PEXISTS_RULE.doc U hol98/src/pair/help/entries/PEXISTS_TAC.doc U hol98/src/pair/help/entries/PEXISTS_UNIQUE_CONV.doc U hol98/src/pair/help/entries/PEXT.doc U hol98/src/pair/help/entries/PFORALL_AND_CONV.doc U hol98/src/pair/help/entries/PFORALL_EQ.doc U hol98/src/pair/help/entries/PFORALL_IMP_CONV.doc U hol98/src/pair/help/entries/PFORALL_NOT_CONV.doc U hol98/src/pair/help/entries/PFORALL_OR_CONV.doc U hol98/src/pair/help/entries/PGEN.doc U hol98/src/pair/help/entries/PGENL.doc U hol98/src/pair/help/entries/PGEN_TAC.doc U hol98/src/pair/help/entries/PMATCH_MP.doc U hol98/src/pair/help/entries/PMATCH_MP_TAC.doc U hol98/src/pair/help/entries/PSELECT_CONV.doc U hol98/src/pair/help/entries/PSELECT_ELIM.doc U hol98/src/pair/help/entries/PSELECT_EQ.doc U hol98/src/pair/help/entries/PSELECT_INTRO.doc U hol98/src/pair/help/entries/PSELECT_RULE.doc U hol98/src/pair/help/entries/PSKOLEM_CONV.doc U hol98/src/pair/help/entries/PSPEC.doc U hol98/src/pair/help/entries/PSPECL.doc U hol98/src/pair/help/entries/PSPEC_ALL.doc U hol98/src/pair/help/entries/PSPEC_PAIR.doc U hol98/src/pair/help/entries/PSPEC_TAC.doc U hol98/src/pair/help/entries/PSTRIP_ASSUME_TAC.doc U hol98/src/pair/help/entries/PSTRIP_GOAL_THEN.doc U hol98/src/pair/help/entries/PSTRIP_TAC.doc U hol98/src/pair/help/entries/PSTRIP_THM_THEN.doc U hol98/src/pair/help/entries/PSTRUCT_CASES_TAC.doc U hol98/src/pair/help/entries/PSUB_CONV.doc U hol98/src/pair/help/entries/P_FUN_EQ_CONV.doc U hol98/src/pair/help/entries/P_PCHOOSE_TAC.doc U hol98/src/pair/help/entries/P_PCHOOSE_THEN.doc U hol98/src/pair/help/entries/P_PGEN_TAC.doc U hol98/src/pair/help/entries/P_PSKOLEM_CONV.doc U hol98/src/pair/help/entries/RIGHT_AND_PEXISTS_CONV.doc U hol98/src/pair/help/entries/RIGHT_AND_PFORALL_CONV.doc U hol98/src/pair/help/entries/RIGHT_IMP_PEXISTS_CONV.doc U hol98/src/pair/help/entries/RIGHT_IMP_PFORALL_CONV.doc U hol98/src/pair/help/entries/RIGHT_LIST_PBETA.doc U hol98/src/pair/help/entries/RIGHT_OR_PEXISTS_CONV.doc U hol98/src/pair/help/entries/RIGHT_OR_PFORALL_CONV.doc U hol98/src/pair/help/entries/RIGHT_PBETA.doc U hol98/src/pair/help/entries/SWAP_PEXISTS_CONV.doc U hol98/src/pair/help/entries/SWAP_PFORALL_CONV.doc U hol98/src/pair/help/entries/UNCURRY_CONV.doc U hol98/src/pair/help/entries/UNCURRY_EXISTS_CONV.doc U hol98/src/pair/help/entries/UNCURRY_FORALL_CONV.doc U hol98/src/pair/help/entries/UNPBETA_CONV.doc U hol98/src/pair/help/entries/bndpair.doc U hol98/src/pair/help/entries/dest_pabs.doc U hol98/src/pair/help/entries/dest_pexists.doc U hol98/src/pair/help/entries/dest_pforall.doc U hol98/src/pair/help/entries/dest_prod.doc U hol98/src/pair/help/entries/dest_pselect.doc U hol98/src/pair/help/entries/genlike.doc U hol98/src/pair/help/entries/is_pabs.doc U hol98/src/pair/help/entries/is_pexists.doc U hol98/src/pair/help/entries/is_pforall.doc U hol98/src/pair/help/entries/is_prod.doc U hol98/src/pair/help/entries/is_pselect.doc U hol98/src/pair/help/entries/is_pvar.doc U hol98/src/pair/help/entries/list_mk_pabs.doc U hol98/src/pair/help/entries/list_mk_pexists-lc.doc U hol98/src/pair/help/entries/list_mk_pforall-lc.doc U hol98/src/pair/help/entries/mk_pabs-lc.doc U hol98/src/pair/help/entries/mk_pexists-lc.doc U hol98/src/pair/help/entries/mk_pforall-lc.doc U hol98/src/pair/help/entries/mk_prod.doc U hol98/src/pair/help/entries/mk_pselect-lc.doc U hol98/src/pair/help/entries/occs_in.doc U hol98/src/pair/help/entries/paconv.doc U hol98/src/pair/help/entries/pbody.doc U hol98/src/pair/help/entries/pvariant.doc U hol98/src/pair/help/entries/rip_pair.doc U hol98/src/pair/help/entries/strip_pabs.doc U hol98/src/pair/help/entries/strip_pexists.doc U hol98/src/pair/help/entries/strip_pforall.doc cvs server: Updating hol98/src/pair/src U hol98/src/pair/src/PairedLambda.sig U hol98/src/pair/src/PairedLambda.sml U hol98/src/pair/src/pairLib.sig U hol98/src/pair/src/pairLib.sml U hol98/src/pair/src/pairScript.sml U hol98/src/pair/src/pairSimps.sig U hol98/src/pair/src/pairSimps.sml U hol98/src/pair/src/pairSyntax.sig U hol98/src/pair/src/pairSyntax.sml U hol98/src/pair/src/pairTools.sig U hol98/src/pair/src/pairTools.sml cvs server: Updating hol98/src/parse U hol98/src/parse/.cvsignore U hol98/src/parse/Absyn.sig U hol98/src/parse/Absyn.sml U hol98/src/parse/GrammarSpecials.sig U hol98/src/parse/GrammarSpecials.sml U hol98/src/parse/HOLgrammars.sig U hol98/src/parse/HOLgrammars.sml U hol98/src/parse/HOLtokens.sig U hol98/src/parse/HOLtokens.sml U hol98/src/parse/Hol_pp.sig U hol98/src/parse/Hol_pp.sml U hol98/src/parse/Literal.sig U hol98/src/parse/Literal.sml U hol98/src/parse/Overload.sig U hol98/src/parse/Overload.sml U hol98/src/parse/Parse.sig U hol98/src/parse/Parse.sml U hol98/src/parse/Parse_support.sig U hol98/src/parse/Parse_support.sml U hol98/src/parse/Preterm.sig U hol98/src/parse/Preterm.sml U hol98/src/parse/Pretype.sig U hol98/src/parse/Pretype.sml U hol98/src/parse/fragstr.sig U hol98/src/parse/fragstr.sml U hol98/src/parse/monadic_parse.sig U hol98/src/parse/monadic_parse.sml U hol98/src/parse/optmonad.sig U hol98/src/parse/optmonad.sml U hol98/src/parse/parse_term.sig U hol98/src/parse/parse_term.sml U hol98/src/parse/parse_type.sig U hol98/src/parse/parse_type.sml U hol98/src/parse/seq.sig U hol98/src/parse/seq.sml U hol98/src/parse/seqmonad.sig U hol98/src/parse/seqmonad.sml U hol98/src/parse/stmonad.sig U hol98/src/parse/stmonad.sml U hol98/src/parse/term_grammar.sig U hol98/src/parse/term_grammar.sml U hol98/src/parse/term_pp.sig U hol98/src/parse/term_pp.sml U hol98/src/parse/term_pp_types.sig U hol98/src/parse/term_pp_types.sml U hol98/src/parse/term_tokens.sig U hol98/src/parse/term_tokens.sml U hol98/src/parse/type_grammar.sig U hol98/src/parse/type_grammar.sml U hol98/src/parse/type_pp.sig U hol98/src/parse/type_pp.sml U hol98/src/parse/type_tokens.sig U hol98/src/parse/type_tokens.sml cvs server: Updating hol98/src/portableML U hol98/src/portableML/Arbint.sig U hol98/src/portableML/Arbint.sml U hol98/src/portableML/Arbnum.sig U hol98/src/portableML/Arbnum.sml U hol98/src/portableML/Holmakefile U hol98/src/portableML/Portable.sig U hol98/src/portableML/Portable.sml U hol98/src/portableML/README cvs server: Updating hol98/src/pred_set U hol98/src/pred_set/CHANGES U hol98/src/pred_set/READ-ME cvs server: Updating hol98/src/pred_set/Manual U hol98/src/pred_set/Manual/Makefile U hol98/src/pred_set/Manual/description.tex U hol98/src/pred_set/Manual/entries-intro.tex U hol98/src/pred_set/Manual/index.tex U hol98/src/pred_set/Manual/pred_sets.tex U hol98/src/pred_set/Manual/references.tex U hol98/src/pred_set/Manual/theorems-intro.tex U hol98/src/pred_set/Manual/title.tex cvs server: Updating hol98/src/pred_set/help cvs server: Updating hol98/src/pred_set/help/entries U hol98/src/pred_set/help/entries/DELETE_CONV.doc U hol98/src/pred_set/help/entries/FINITE_CONV.doc U hol98/src/pred_set/help/entries/IMAGE_CONV.doc U hol98/src/pred_set/help/entries/INSERT_CONV.doc U hol98/src/pred_set/help/entries/IN_CONV.doc U hol98/src/pred_set/help/entries/SET_INDUCT_TAC.doc U hol98/src/pred_set/help/entries/SET_SPEC_CONV.doc U hol98/src/pred_set/help/entries/UNION_CONV.doc cvs server: Updating hol98/src/pred_set/src U hol98/src/pred_set/src/PFset_conv.sig U hol98/src/pred_set/src/PFset_conv.sml U hol98/src/pred_set/src/PGspec.sig U hol98/src/pred_set/src/PGspec.sml U hol98/src/pred_set/src/PSet_ind.sig U hol98/src/pred_set/src/PSet_ind.sml U hol98/src/pred_set/src/pred_setLib.sig U hol98/src/pred_set/src/pred_setLib.sml U hol98/src/pred_set/src/pred_setScript.sml U hol98/src/pred_set/src/pred_setSimps.sig U hol98/src/pred_set/src/pred_setSimps.sml cvs server: Updating hol98/src/prob U hol98/src/prob/boolean_sequenceScript.sml U hol98/src/prob/boolean_sequenceTools.sig U hol98/src/prob/boolean_sequenceTools.sml U hol98/src/prob/probLib.sig U hol98/src/prob/probLib.sml U hol98/src/prob/probScript.sml U hol98/src/prob/probTools.sig U hol98/src/prob/probTools.sml U hol98/src/prob/probUtil.sig U hol98/src/prob/probUtil.sml U hol98/src/prob/prob_algebraScript.sml U hol98/src/prob/prob_canonScript.sml U hol98/src/prob/prob_canonTools.sig U hol98/src/prob/prob_canonTools.sml U hol98/src/prob/prob_extraScript.sml U hol98/src/prob/prob_extraTools.sig U hol98/src/prob/prob_extraTools.sml U hol98/src/prob/prob_indepScript.sml U hol98/src/prob/prob_pseudoScript.sml U hol98/src/prob/prob_pseudoTools.sig U hol98/src/prob/prob_pseudoTools.sml U hol98/src/prob/prob_uniformScript.sml U hol98/src/prob/prob_uniformTools.sig U hol98/src/prob/prob_uniformTools.sml U hol98/src/prob/state_transformerScript.sml cvs server: Updating hol98/src/q U hol98/src/q/Q.sig U hol98/src/q/Q.sml U hol98/src/q/QLib.sml U hol98/src/q/README cvs server: Updating hol98/src/quote-filter U hol98/src/quote-filter/Makefile U hol98/src/quote-filter/Makefile.0 U hol98/src/quote-filter/QuoteFilter.sml U hol98/src/quote-filter/filter.lex U hol98/src/quote-filter/filter.lex.0 U hol98/src/quote-filter/hol_filt.exe cvs server: Updating hol98/src/real U hol98/src/real/Diff.sig U hol98/src/real/Diff.sml U hol98/src/real/RealArith.sig U hol98/src/real/RealArith.sml U hol98/src/real/analysis.ml U hol98/src/real/hratScript.sml U hol98/src/real/hrealScript.sml U hol98/src/real/limScript.sml U hol98/src/real/netsScript.sml U hol98/src/real/polyScript.sml U hol98/src/real/powserScript.sml U hol98/src/real/realLib.sig U hol98/src/real/realLib.sml U hol98/src/real/realScript.sml U hol98/src/real/realSimps.sig U hol98/src/real/realSimps.sml U hol98/src/real/realaxScript.sml U hol98/src/real/seqScript.sml U hol98/src/real/topologyScript.sml U hol98/src/real/transc.ml U hol98/src/real/transcScript.sml cvs server: Updating hol98/src/reduce cvs server: Updating hol98/src/reduce/Manual cvs server: Updating hol98/src/reduce/help cvs server: Updating hol98/src/reduce/help/entries cvs server: Updating hol98/src/reduce/src cvs server: Updating hol98/src/refute U hol98/src/refute/AC.sig U hol98/src/refute/AC.sml U hol98/src/refute/Canon.sig U hol98/src/refute/Canon.sml U hol98/src/refute/READ-ME U hol98/src/refute/refuteLib.sig U hol98/src/refute/refuteLib.sml cvs server: Updating hol98/src/relation U hol98/src/relation/relationScript.sml cvs server: Updating hol98/src/res_quan cvs server: Updating hol98/src/res_quan/Manual U hol98/src/res_quan/Manual/Makefile U hol98/src/res_quan/Manual/description.tex U hol98/src/res_quan/Manual/entries-intro.tex U hol98/src/res_quan/Manual/index.tex U hol98/src/res_quan/Manual/res_quan.tex U hol98/src/res_quan/Manual/summacs.tex U hol98/src/res_quan/Manual/summary.tex U hol98/src/res_quan/Manual/theorems-intro.tex U hol98/src/res_quan/Manual/title.tex cvs server: Updating hol98/src/res_quan/help cvs server: Updating hol98/src/res_quan/help/entries U hol98/src/res_quan/help/entries/COND_REWRITE1_CONV.doc U hol98/src/res_quan/help/entries/COND_REWRITE1_TAC.doc U hol98/src/res_quan/help/entries/COND_REWR_CANON.doc U hol98/src/res_quan/help/entries/COND_REWR_CONV.doc U hol98/src/res_quan/help/entries/COND_REWR_TAC.doc U hol98/src/res_quan/help/entries/GQSPECL.doc U hol98/src/res_quan/help/entries/GQSPEC_ALL.doc U hol98/src/res_quan/help/entries/IMP_RESQ_FORALL_CONV.doc U hol98/src/res_quan/help/entries/LIST_RESQ_FORALL_CONV.doc U hol98/src/res_quan/help/entries/RESQ_EXISTS_CONV.doc U hol98/src/res_quan/help/entries/RESQ_EXISTS_TAC.doc U hol98/src/res_quan/help/entries/RESQ_FORALL_AND_CONV.doc U hol98/src/res_quan/help/entries/RESQ_FORALL_CONV.doc U hol98/src/res_quan/help/entries/RESQ_FORALL_SWAP_CONV.doc U hol98/src/res_quan/help/entries/RESQ_GEN.doc U hol98/src/res_quan/help/entries/RESQ_GENL.doc U hol98/src/res_quan/help/entries/RESQ_GEN_ALL.doc U hol98/src/res_quan/help/entries/RESQ_GEN_TAC.doc U hol98/src/res_quan/help/entries/RESQ_HALF_EXISTS.doc U hol98/src/res_quan/help/entries/RESQ_HALF_GEN_TAC.doc U hol98/src/res_quan/help/entries/RESQ_HALF_SPEC.doc U hol98/src/res_quan/help/entries/RESQ_IMP_RES_TAC.doc U hol98/src/res_quan/help/entries/RESQ_IMP_RES_THEN.doc U hol98/src/res_quan/help/entries/RESQ_MATCH_MP.doc U hol98/src/res_quan/help/entries/RESQ_RES_TAC.doc U hol98/src/res_quan/help/entries/RESQ_RES_THEN.doc U hol98/src/res_quan/help/entries/RESQ_REWRITE1_CONV.doc U hol98/src/res_quan/help/entries/RESQ_REWRITE1_TAC.doc U hol98/src/res_quan/help/entries/RESQ_REWR_CANON.doc U hol98/src/res_quan/help/entries/RESQ_SPEC.doc U hol98/src/res_quan/help/entries/RESQ_SPECL.doc U hol98/src/res_quan/help/entries/RESQ_SPEC_ALL.doc U hol98/src/res_quan/help/entries/dest_resq_abstract.doc U hol98/src/res_quan/help/entries/dest_resq_exists.doc U hol98/src/res_quan/help/entries/dest_resq_forall.doc U hol98/src/res_quan/help/entries/dest_resq_select.doc U hol98/src/res_quan/help/entries/is_resq_abstract.doc U hol98/src/res_quan/help/entries/is_resq_exists.doc U hol98/src/res_quan/help/entries/is_resq_forall.doc U hol98/src/res_quan/help/entries/is_resq_select.doc U hol98/src/res_quan/help/entries/list_mk_resq_exists.doc U hol98/src/res_quan/help/entries/list_mk_resq_forall.doc U hol98/src/res_quan/help/entries/mk_resq_abstract.doc U hol98/src/res_quan/help/entries/mk_resq_exists.doc U hol98/src/res_quan/help/entries/mk_resq_forall.doc U hol98/src/res_quan/help/entries/mk_resq_select.doc U hol98/src/res_quan/help/entries/new_binder_resq_definition.doc U hol98/src/res_quan/help/entries/new_infix_resq_definition.doc U hol98/src/res_quan/help/entries/new_resq_definition.doc U hol98/src/res_quan/help/entries/search_top_down.doc U hol98/src/res_quan/help/entries/strip_resq_exists.doc U hol98/src/res_quan/help/entries/strip_resq_forall.doc cvs server: Updating hol98/src/res_quan/src U hol98/src/res_quan/src/Cond_rewrite.sig U hol98/src/res_quan/src/Cond_rewrite.sml U hol98/src/res_quan/src/Res_quan.sig U hol98/src/res_quan/src/Res_quan.sml U hol98/src/res_quan/src/res_quanLib.sig U hol98/src/res_quan/src/res_quanLib.sml U hol98/src/res_quan/src/res_quanScript.sml cvs server: Updating hol98/src/res_quan/theories cvs server: Updating hol98/src/ring cvs server: Updating hol98/src/ring/examples U hol98/src/ring/examples/tests.sml cvs server: Updating hol98/src/ring/help cvs server: Updating hol98/src/ring/help/entries U hol98/src/ring/help/entries/declare_ring.doc cvs server: Updating hol98/src/ring/src U hol98/src/ring/src/abs_tools.sml U hol98/src/ring/src/abstraction.sig U hol98/src/ring/src/abstraction.sml U hol98/src/ring/src/canonicalScript.sml U hol98/src/ring/src/integerRingLib.sig U hol98/src/ring/src/integerRingLib.sml U hol98/src/ring/src/integerRingScript.sml U hol98/src/ring/src/numRingLib.sig U hol98/src/ring/src/numRingLib.sml U hol98/src/ring/src/numRingScript.sml U hol98/src/ring/src/prelimScript.sml U hol98/src/ring/src/quote.sml U hol98/src/ring/src/quoteScript.sml U hol98/src/ring/src/ringLib.sig U hol98/src/ring/src/ringLib.sml U hol98/src/ring/src/ringNormScript.sml U hol98/src/ring/src/ringScript.sml U hol98/src/ring/src/semi_ringScript.sml cvs server: Updating hol98/src/robdd cvs server: Updating hol98/src/robdd/buddy16 cvs server: Updating hol98/src/robdd/buddy16/doc cvs server: Updating hol98/src/robdd/buddy16/examples cvs server: Updating hol98/src/robdd/buddy16/examples/adder cvs server: Updating hol98/src/robdd/buddy16/examples/cmilner cvs server: Updating hol98/src/robdd/buddy16/examples/milner cvs server: Updating hol98/src/robdd/buddy16/examples/queen cvs server: Updating hol98/src/robdd/buddy16/src cvs server: Updating hol98/src/set cvs server: Updating hol98/src/set/Manual U hol98/src/set/Manual/Makefile U hol98/src/set/Manual/description.tex U hol98/src/set/Manual/entries-intro.tex U hol98/src/set/Manual/index.tex U hol98/src/set/Manual/references.tex U hol98/src/set/Manual/sets.tex U hol98/src/set/Manual/theorems-intro.tex U hol98/src/set/Manual/theorems.tex U hol98/src/set/Manual/title.tex cvs server: Updating hol98/src/set/help cvs server: Updating hol98/src/set/help/entries U hol98/src/set/help/entries/DELETE_CONV.doc U hol98/src/set/help/entries/FINITE_CONV.doc U hol98/src/set/help/entries/IMAGE_CONV.doc U hol98/src/set/help/entries/INSERT_CONV.doc U hol98/src/set/help/entries/IN_CONV.doc U hol98/src/set/help/entries/SET_INDUCT_TAC.doc U hol98/src/set/help/entries/SET_SPEC_CONV.doc U hol98/src/set/help/entries/UNION_CONV.doc cvs server: Updating hol98/src/set/src U hol98/src/set/src/Fset_conv.sig U hol98/src/set/src/Fset_conv.sml U hol98/src/set/src/Gspec.sig U hol98/src/set/src/Gspec.sml U hol98/src/set/src/Set_ind.sig U hol98/src/set/src/Set_ind.sml U hol98/src/set/src/finsetScript.sml U hol98/src/set/src/setLib.sig U hol98/src/set/src/setLib.sml U hol98/src/set/src/setScript.sml U hol98/src/set/src/setSimps.sig U hol98/src/set/src/setSimps.sml cvs server: Updating hol98/src/simp U hol98/src/simp/READ-ME U hol98/src/simp/test.sml cvs server: Updating hol98/src/simp/doc U hol98/src/simp/doc/commands.tex U hol98/src/simp/doc/simp.tex cvs server: Updating hol98/src/simp/doc/misc U hol98/src/simp/doc/misc/dproc.tex U hol98/src/simp/doc/misc/frags.tex U hol98/src/simp/doc/misc/junk.tex cvs server: Updating hol98/src/simp/src U hol98/src/simp/src/Cache.sig U hol98/src/simp/src/Cache.sml U hol98/src/simp/src/Cond_rewr.sig U hol98/src/simp/src/Cond_rewr.sml U hol98/src/simp/src/Opening.sig U hol98/src/simp/src/Opening.sml U hol98/src/simp/src/Satisfy.sig U hol98/src/simp/src/Satisfy.sml U hol98/src/simp/src/SatisfySimps.sig U hol98/src/simp/src/SatisfySimps.sml U hol98/src/simp/src/Sequence.sig U hol98/src/simp/src/Sequence.sml U hol98/src/simp/src/Trace.sig U hol98/src/simp/src/Trace.sml U hol98/src/simp/src/Traverse.sig U hol98/src/simp/src/Traverse.sml U hol98/src/simp/src/Travrules.sig U hol98/src/simp/src/Travrules.sml U hol98/src/simp/src/Unify.sig U hol98/src/simp/src/Unify.sml U hol98/src/simp/src/Unwind.sig U hol98/src/simp/src/Unwind.sml U hol98/src/simp/src/boolSimps.sig U hol98/src/simp/src/boolSimps.sml U hol98/src/simp/src/combinSimps.sig U hol98/src/simp/src/combinSimps.sml U hol98/src/simp/src/pureSimps.sig U hol98/src/simp/src/pureSimps.sml U hol98/src/simp/src/simpLib.sig U hol98/src/simp/src/simpLib.sml cvs server: Updating hol98/src/string U hol98/src/string/READ-ME U hol98/src/string/stringLib.sig U hol98/src/string/stringLib.sml U hol98/src/string/stringScript.sml U hol98/src/string/stringSimps.sig U hol98/src/string/stringSimps.sml U hol98/src/string/stringSyntax.sig U hol98/src/string/stringSyntax.sml cvs server: Updating hol98/src/string/Manual U hol98/src/string/Manual/Makefile U hol98/src/string/Manual/description.tex U hol98/src/string/Manual/entries-intro.tex U hol98/src/string/Manual/index.tex U hol98/src/string/Manual/references.tex U hol98/src/string/Manual/string.tex U hol98/src/string/Manual/theorems-intro.tex U hol98/src/string/Manual/title.tex cvs server: Updating hol98/src/string/help cvs server: Updating hol98/src/string/help/entries U hol98/src/string/help/entries/ascii_EQ_CONV.doc U hol98/src/string/help/entries/string_CONV.doc U hol98/src/string/help/entries/string_EQ_CONV.doc cvs server: Updating hol98/src/string/src cvs server: Updating hol98/src/string/theories cvs server: Updating hol98/src/sum U hol98/src/sum/sumScript.sml U hol98/src/sum/sumSimps.sig U hol98/src/sum/sumSimps.sml U hol98/src/sum/sumSyntax.sig U hol98/src/sum/sumSyntax.sml cvs server: Updating hol98/src/taut U hol98/src/taut/READ-ME U hol98/src/taut/tautLib.sig U hol98/src/taut/tautLib.sml cvs server: Updating hol98/src/taut/Manual U hol98/src/taut/Manual/Makefile U hol98/src/taut/Manual/description.tex U hol98/src/taut/Manual/entries-intro.tex U hol98/src/taut/Manual/index.tex U hol98/src/taut/Manual/references.tex U hol98/src/taut/Manual/taut.tex U hol98/src/taut/Manual/title.tex cvs server: Updating hol98/src/taut/help cvs server: Updating hol98/src/taut/help/entries U hol98/src/taut/help/entries/PTAUT_CONV.doc U hol98/src/taut/help/entries/PTAUT_PROVE.doc U hol98/src/taut/help/entries/PTAUT_TAC.doc U hol98/src/taut/help/entries/TAUT_CONV.doc U hol98/src/taut/help/entries/TAUT_PROVE.doc U hol98/src/taut/help/entries/TAUT_TAC.doc cvs server: Updating hol98/src/temporal U hol98/src/temporal/INSTALL U hol98/src/temporal/README U hol98/src/temporal/examples.sml cvs server: Updating hol98/src/temporal/smv.2.4.3 U hol98/src/temporal/smv.2.4.3/assoc.c U hol98/src/temporal/smv.2.4.3/assoc.h U hol98/src/temporal/smv.2.4.3/bdd.c U hol98/src/temporal/smv.2.4.3/bdd.h U hol98/src/temporal/smv.2.4.3/grammar.y U hol98/src/temporal/smv.2.4.3/hash.c U hol98/src/temporal/smv.2.4.3/hash.h U hol98/src/temporal/smv.2.4.3/input.lex U hol98/src/temporal/smv.2.4.3/main.c U hol98/src/temporal/smv.2.4.3/makefile U hol98/src/temporal/smv.2.4.3/node.c U hol98/src/temporal/smv.2.4.3/node.h U hol98/src/temporal/smv.2.4.3/smv.1 U hol98/src/temporal/smv.2.4.3/storage.c U hol98/src/temporal/smv.2.4.3/storage.h U hol98/src/temporal/smv.2.4.3/string.c U hol98/src/temporal/smv.2.4.3/string.h U hol98/src/temporal/smv.2.4.3/symbols.c cvs server: Updating hol98/src/temporal/smv.2.4.3/doc cvs server: Updating hol98/src/temporal/smv.2.4.3/examples cvs server: Updating hol98/src/temporal/src U hol98/src/temporal/src/Omega_AutomataScript.sml U hol98/src/temporal/src/Past_Temporal_LogicScript.sml U hol98/src/temporal/src/Temporal_LogicScript.sml U hol98/src/temporal/src/schneiderUtils.sig U hol98/src/temporal/src/schneiderUtils.sml U hol98/src/temporal/src/temporalLib.sig U hol98/src/temporal/src/temporalLib.sml cvs server: Updating hol98/src/tfl cvs server: Updating hol98/src/tfl/doc U hol98/src/tfl/doc/CHANGES U hol98/src/tfl/doc/README U hol98/src/tfl/doc/doc.txt U hol98/src/tfl/doc/tfl.announce cvs server: Updating hol98/src/tfl/examples U hol98/src/tfl/examples/91 U hol98/src/tfl/examples/Cbags U hol98/src/tfl/examples/cond U hol98/src/tfl/examples/ctl U hol98/src/tfl/examples/exp U hol98/src/tfl/examples/fusion U hol98/src/tfl/examples/iota U hol98/src/tfl/examples/it_prim_rec U hol98/src/tfl/examples/jones U hol98/src/tfl/examples/kapur_subra U hol98/src/tfl/examples/lcf.example U hol98/src/tfl/examples/linRec U hol98/src/tfl/examples/mutrec U hol98/src/tfl/examples/proplog U hol98/src/tfl/examples/scheme.nested U hol98/src/tfl/examples/setlist U hol98/src/tfl/examples/subst.list U hol98/src/tfl/examples/subst.set U hol98/src/tfl/examples/test.Define U hol98/src/tfl/examples/variant U hol98/src/tfl/examples/while cvs server: Updating hol98/src/tfl/examples/sorting U hol98/src/tfl/examples/sorting/flag U hol98/src/tfl/examples/sorting/fqsort U hol98/src/tfl/examples/sorting/minsort U hol98/src/tfl/examples/sorting/partitionScript.sml U hol98/src/tfl/examples/sorting/permScript.sml U hol98/src/tfl/examples/sorting/qsort U hol98/src/tfl/examples/sorting/qsort.compute U hol98/src/tfl/examples/sorting/samsort U hol98/src/tfl/examples/sorting/sortingScript.sml cvs server: Updating hol98/src/tfl/src U hol98/src/tfl/src/.cvsignore U hol98/src/tfl/src/Defn.sig U hol98/src/tfl/src/Defn.sml U hol98/src/tfl/src/Functional.sig U hol98/src/tfl/src/Functional.sml U hol98/src/tfl/src/Induction.sig U hol98/src/tfl/src/Induction.sml U hol98/src/tfl/src/RW.sig U hol98/src/tfl/src/RW.sml U hol98/src/tfl/src/Rules.sig U hol98/src/tfl/src/Rules.sml U hol98/src/tfl/src/TotalDefn.sig U hol98/src/tfl/src/TotalDefn.sml U hol98/src/tfl/src/wfrecUtils.sig U hol98/src/tfl/src/wfrecUtils.sml cvs server: Updating hol98/src/tfl/src/test U hol98/src/tfl/src/test/test.97.sml U hol98/src/tfl/src/test/test.98.sml U hol98/src/tfl/src/test/test.nest U hol98/src/tfl/src/test/test.sml U hol98/src/tfl/src/test/test1.sml U hol98/src/tfl/src/test/test2.sml cvs server: Updating hol98/src/tree U hol98/src/tree/ltreeScript.sml U hol98/src/tree/treeScript.sml cvs server: Updating hol98/src/unwind U hol98/src/unwind/CHANGES U hol98/src/unwind/READ-ME U hol98/src/unwind/unwindLib.sig U hol98/src/unwind/unwindLib.sml cvs server: Updating hol98/src/unwind/Manual U hol98/src/unwind/Manual/Makefile U hol98/src/unwind/Manual/description.tex U hol98/src/unwind/Manual/entries-intro.tex U hol98/src/unwind/Manual/entries.tex U hol98/src/unwind/Manual/index.tex U hol98/src/unwind/Manual/references.tex U hol98/src/unwind/Manual/title.tex U hol98/src/unwind/Manual/unwind.tex cvs server: Updating hol98/src/unwind/help cvs server: Updating hol98/src/unwind/help/entries U hol98/src/unwind/help/entries/CONJ_FORALL_CONV.doc U hol98/src/unwind/help/entries/CONJ_FORALL_ONCE_CONV.doc U hol98/src/unwind/help/entries/CONJ_FORALL_RIGHT_RULE.doc U hol98/src/unwind/help/entries/DEPTH_EXISTS_CONV.doc U hol98/src/unwind/help/entries/DEPTH_FORALL_CONV.doc U hol98/src/unwind/help/entries/EXISTS_DEL1_CONV.doc U hol98/src/unwind/help/entries/EXISTS_DEL_CONV.doc U hol98/src/unwind/help/entries/EXISTS_EQN_CONV.doc U hol98/src/unwind/help/entries/EXPAND_ALL_BUT_CONV.doc U hol98/src/unwind/help/entries/EXPAND_ALL_BUT_RIGHT_RULE.doc U hol98/src/unwind/help/entries/EXPAND_AUTO_CONV.doc U hol98/src/unwind/help/entries/EXPAND_AUTO_RIGHT_RULE.doc U hol98/src/unwind/help/entries/FLATTEN_CONJ_CONV.doc U hol98/src/unwind/help/entries/FORALL_CONJ_CONV.doc U hol98/src/unwind/help/entries/FORALL_CONJ_ONCE_CONV.doc U hol98/src/unwind/help/entries/FORALL_CONJ_RIGHT_RULE.doc U hol98/src/unwind/help/entries/PRUNE_CONV.doc U hol98/src/unwind/help/entries/PRUNE_ONCE_CONV.doc U hol98/src/unwind/help/entries/PRUNE_ONE_CONV.doc U hol98/src/unwind/help/entries/PRUNE_RIGHT_RULE.doc U hol98/src/unwind/help/entries/PRUNE_SOME_CONV.doc U hol98/src/unwind/help/entries/PRUNE_SOME_RIGHT_RULE.doc U hol98/src/unwind/help/entries/UNFOLD_CONV.doc U hol98/src/unwind/help/entries/UNFOLD_RIGHT_RULE.doc U hol98/src/unwind/help/entries/UNWIND_ALL_BUT_CONV.doc U hol98/src/unwind/help/entries/UNWIND_ALL_BUT_RIGHT_RULE.doc U hol98/src/unwind/help/entries/UNWIND_AUTO_CONV.doc U hol98/src/unwind/help/entries/UNWIND_AUTO_RIGHT_RULE.doc U hol98/src/unwind/help/entries/UNWIND_CONV.doc U hol98/src/unwind/help/entries/UNWIND_ONCE_CONV.doc U hol98/src/unwind/help/entries/line_name.doc U hol98/src/unwind/help/entries/line_var.doc cvs server: Updating hol98/src/utils cvs server: Updating hol98/src/utils/help U hol98/src/utils/help/ASSUM_LIST_TAC.doc U hol98/src/utils/help/MP_IMP_TAC.doc U hol98/src/utils/help/NEW_SUBST1_TAC.doc U hol98/src/utils/help/REV_SUPPOSE_TAC.doc U hol98/src/utils/help/SUBST_MATCH_TAC.doc U hol98/src/utils/help/SUPPOSE_TAC.doc cvs server: Updating hol98/src/word cvs server: Updating hol98/src/word/Manual U hol98/src/word/Manual/Makefile U hol98/src/word/Manual/cmssc12.tfm U hol98/src/word/Manual/cmssc12.vf U hol98/src/word/Manual/description.tex U hol98/src/word/Manual/entries-intro.tex U hol98/src/word/Manual/holmacs.tex U hol98/src/word/Manual/index.tex U hol98/src/word/Manual/macros.tex U hol98/src/word/Manual/model_word.tex U hol98/src/word/Manual/theorems-intro.tex U hol98/src/word/Manual/thy_hier.tex U hol98/src/word/Manual/title.tex U hol98/src/word/Manual/tokmac.tex U hol98/src/word/Manual/word.bbl U hol98/src/word/Manual/word.tex cvs server: Updating hol98/src/word/help cvs server: Updating hol98/src/word/help/entries U hol98/src/word/help/entries/BIT_CONV.doc U hol98/src/word/help/entries/PWORDLEN_CONV.doc U hol98/src/word/help/entries/PWORDLEN_TAC.doc U hol98/src/word/help/entries/PWORDLEN_bitop_CONV.doc U hol98/src/word/help/entries/WSEG_CONV.doc U hol98/src/word/help/entries/WSEG_WSEG_CONV.doc cvs server: Updating hol98/src/word/src U hol98/src/word/src/wordLib.sig U hol98/src/word/src/wordLib.sml cvs server: Updating hol98/src/word/theories U hol98/src/word/theories/Base.sml U hol98/src/word/theories/bword_arithScript.sml U hol98/src/word/theories/bword_bitopScript.sml U hol98/src/word/theories/bword_numScript.sml U hol98/src/word/theories/wordScript.sml U hol98/src/word/theories/word_baseScript.sml U hol98/src/word/theories/word_bitopScript.sml U hol98/src/word/theories/word_numScript.sml cvs server: Updating hol98/tools U hol98/tools/Globals.src U hol98/tools/Holmakefile.help.src U hol98/tools/build.src U hol98/tools/config-muddy.sml U hol98/tools/config-unix.sml U hol98/tools/config-winNT.sml U hol98/tools/configure.sml U hol98/tools/documentation-directories U hol98/tools/end-init.sml U hol98/tools/hol98-mode.src U hol98/tools/makebase.src U hol98/tools/makefile.muddy.src U hol98/tools/std.prelude.src U hol98/tools/unquote-init.sml cvs server: Updating hol98/tools/Holmake U hol98/tools/Holmake/Holdep.sml U hol98/tools/Holmake/Holmake.src U hol98/tools/Holmake/Holmake_parse.grm U hol98/tools/Holmake/Holmake_rules.sig U hol98/tools/Holmake/Holmake_rules.sml U hol98/tools/Holmake/Holmake_tokens.lex U hol98/tools/Holmake/Holmake_types.sig U hol98/tools/Holmake/Holmake_types.sml U hol98/tools/Holmake/Lexer.lex U hol98/tools/Holmake/Makefile U hol98/tools/Holmake/Parser.grm U hol98/tools/Holmake/fake_src.pl cvs server: Updating hol98/tools/helpdb U hol98/tools/helpdb/DBparse.grm U hol98/tools/helpdb/DBtokens.lex U hol98/tools/helpdb/DBtokens.sig U hol98/tools/helpdb/Database.sig U hol98/tools/helpdb/Database.sml U hol98/tools/helpdb/build_db.sml U hol98/tools/helpdb/mk_helpdb.sml cvs server: Updating hol98/tools/win-binaries bass%