package info
(click to toggle)
Folder: Help
 |
.. (parent) | |||
 |
- | rw-r--r-- | 977 | .joinparsers.hlp |
|
- | rw-r--r-- | 1,001 | .orparser.hlp |
|
- | rw-r--r-- | 928 | .pipeparser.hlp |
|
- | rw-r--r-- | 775 | .singlefun.hlp |
|
- | rw-r--r-- | 409 | .upto.hlp |
|
- | rw-r--r-- | 962 | .valmod.hlp |
|
- | rw-r--r-- | 1,059 | ABBREV_TAC.hlp |
|
- | rw-r--r-- | 542 | ABS.hlp |
|
- | rw-r--r-- | 1,037 | ABS_CONV.hlp |
|
- | rw-r--r-- | 688 | ABS_TAC.hlp |
|
- | rw-r--r-- | 1,967 | AC.hlp |
|
- | rw-r--r-- | 909 | ACCEPT_TAC.hlp |
|
- | rw-r--r-- | 769 | ADD_ASSUM.hlp |
|
- | rw-r--r-- | 392 | ALL_CONV.hlp |
|
- | rw-r--r-- | 1,128 | ALL_TAC.hlp |
|
- | rw-r--r-- | 715 | ALL_THEN.hlp |
|
- | rw-r--r-- | 875 | ALPHA_CONV.hlp |
|
- | rw-r--r-- | 621 | ALPHA_UPPERCASE.hlp |
|
- | rw-r--r-- | 1,656 | ANTE_RES_THEN.hlp |
|
- | rw-r--r-- | 394 | ANTS_TAC.hlp |
|
- | rw-r--r-- | 673 | AP_TERM.hlp |
|
- | rw-r--r-- | 543 | AP_TERM_TAC.hlp |
|
- | rw-r--r-- | 717 | AP_THM.hlp |
|
- | rw-r--r-- | 579 | AP_THM_TAC.hlp |
|
- | rw-r--r-- | 1,067 | ARITH_RULE.hlp |
|
- | rw-r--r-- | 807 | ARITH_TAC.hlp |
|
- | rw-r--r-- | 584 | ASM.hlp |
|
- | rw-r--r-- | 1,344 | ASM_ARITH_TAC.hlp |
|
- | rw-r--r-- | 1,055 | ASM_CASES_TAC.hlp |
|
- | rw-r--r-- | 906 | ASM_FOL_TAC.hlp |
|
- | rw-r--r-- | 1,488 | ASM_INT_ARITH_TAC.hlp |
|
- | rw-r--r-- | 710 | ASM_MESON_TAC.hlp |
|
- | rw-r--r-- | 642 | ASM_METIS_TAC.hlp |
|
- | rw-r--r-- | 1,809 | ASM_REAL_ARITH_TAC.hlp |
|
- | rw-r--r-- | 980 | ASM_REWRITE_RULE.hlp |
|
- | rw-r--r-- | 1,698 | ASM_REWRITE_TAC.hlp |
|
- | rw-r--r-- | 736 | ASM_SIMP_TAC.hlp |
|
- | rw-r--r-- | 1,100 | ASSOC_CONV.hlp |
|
- | rw-r--r-- | 499 | ASSUME.hlp |
|
- | rw-r--r-- | 1,616 | ASSUME_TAC.hlp |
|
- | rw-r--r-- | 1,308 | ASSUM_LIST.hlp |
|
- | rw-r--r-- | 696 | AUGMENT_SIMPSET.hlp |
|
- | rw-r--r-- | 1,101 | BETA.hlp |
|
- | rw-r--r-- | 478 | BETAS_CONV.hlp |
|
- | rw-r--r-- | 1,070 | BETA_CONV.hlp |
|
- | rw-r--r-- | 871 | BETA_RULE.hlp |
|
- | rw-r--r-- | 834 | BETA_TAC.hlp |
|
- | rw-r--r-- | 851 | BINDER_CONV.hlp |
|
- | rw-r--r-- | 923 | BINOP2_CONV.hlp |
|
- | rw-r--r-- | 750 | BINOP_CONV.hlp |
|
- | rw-r--r-- | 1,184 | BINOP_TAC.hlp |
|
- | rw-r--r-- | 910 | BITS_ELIM_CONV.hlp |
|
- | rw-r--r-- | 1,452 | BOOL_CASES_TAC.hlp |
|
- | rw-r--r-- | 225 | C.hlp |
|
- | rw-r--r-- | 1,149 | CACHE_CONV.hlp |
|
- | rw-r--r-- | 1,417 | CASE_REWRITE_TAC.hlp |
|
- | rw-r--r-- | 676 | CCONTR.hlp |
|
- | rw-r--r-- | 1,287 | CHANGED_CONV.hlp |
|
- | rw-r--r-- | 617 | CHANGED_TAC.hlp |
|
- | rw-r--r-- | 1,139 | CHAR_EQ_CONV.hlp |
|
- | rw-r--r-- | 559 | CHEAT_TAC.hlp |
|
- | rw-r--r-- | 1,152 | CHOOSE_TAC.hlp |
|
- | rw-r--r-- | 1,525 | CHOOSE_THEN.hlp |
|
- | rw-r--r-- | 997 | CHOOSE_UPPERCASE.hlp |
|
- | rw-r--r-- | 1,380 | CLAIM_TAC.hlp |
|
- | rw-r--r-- | 963 | CNF_CONV.hlp |
|
- | rw-r--r-- | 808 | COMB2_CONV.hlp |
|
- | rw-r--r-- | 624 | COMB_CONV.hlp |
|
- | rw-r--r-- | 1,576 | CONDS_CELIM_CONV.hlp |
|
- | rw-r--r-- | 1,701 | CONDS_ELIM_CONV.hlp |
|
- | rw-r--r-- | 2,100 | COND_CASES_TAC.hlp |
|
- | rw-r--r-- | 1,701 | COND_ELIM_CONV.hlp |
|
- | rw-r--r-- | 403 | CONJ.hlp |
|
- | rw-r--r-- | 393 | CONJUNCT1.hlp |
|
- | rw-r--r-- | 394 | CONJUNCT2.hlp |
|
- | rw-r--r-- | 1,316 | CONJUNCTS_THEN.hlp |
|
- | rw-r--r-- | 1,118 | CONJUNCTS_THEN2.hlp |
|
- | rw-r--r-- | 679 | CONJUNCTS_UPPERCASE.hlp |
|
- | rw-r--r-- | 961 | CONJ_ACI_RULE.hlp |
|
- | rw-r--r-- | 774 | CONJ_CANON_CONV.hlp |
|
- | rw-r--r-- | 509 | CONJ_PAIR.hlp |
|
- | rw-r--r-- | 468 | CONJ_TAC.hlp |
|
- | rw-r--r-- | 622 | CONTR.hlp |
|
- | rw-r--r-- | 516 | CONTRAPOS_CONV.hlp |
|
- | rw-r--r-- | 604 | CONTR_TAC.hlp |
|
- | rw-r--r-- | 1,080 | CONV_RULE.hlp |
|
- | rw-r--r-- | 2,281 | CONV_TAC.hlp |
|
- | rw-r--r-- | 951 | DEDUCT_ANTISYM_RULE.hlp |
|
- | rw-r--r-- | 417 | DENUMERAL.hlp |
|
- | rw-r--r-- | 1,492 | DEPTH_BINOP_CONV.hlp |
|
- | rw-r--r-- | 2,474 | DEPTH_CONV.hlp |
|
- | rw-r--r-- | 577 | DEPTH_SQCONV.hlp |
|
- | rw-r--r-- | 1,958 | DESTRUCT_TAC.hlp |
|
- | rw-r--r-- | 836 | DIMINDEX_CONV.hlp |
|
- | rw-r--r-- | 654 | DIMINDEX_TAC.hlp |
|
- | rw-r--r-- | 598 | DISCH.hlp |
|
- | rw-r--r-- | 922 | DISCH_ALL.hlp |
|
- | rw-r--r-- | 801 | DISCH_TAC.hlp |
|
- | rw-r--r-- | 1,385 | DISCH_THEN.hlp |
|
- | rw-r--r-- | 414 | DISJ1.hlp |
|
- | rw-r--r-- | 303 | DISJ1_TAC.hlp |
|
- | rw-r--r-- | 402 | DISJ2.hlp |
|
- | rw-r--r-- | 308 | DISJ2_TAC.hlp |
|
- | rw-r--r-- | 945 | DISJ_ACI_RULE.hlp |
|
- | rw-r--r-- | 768 | DISJ_CANON_CONV.hlp |
|
- | rw-r--r-- | 1,648 | DISJ_CASES.hlp |
|
- | rw-r--r-- | 1,192 | DISJ_CASES_TAC.hlp |
|
- | rw-r--r-- | 1,881 | DISJ_CASES_THEN.hlp |
|
- | rw-r--r-- | 2,185 | DISJ_CASES_THEN2.hlp |
|
- | rw-r--r-- | 918 | DNF_CONV.hlp |
|
- | rw-r--r-- | 792 | EL_CONV.hlp |
|
- | rw-r--r-- | 418 | EQF_ELIM.hlp |
|
- | rw-r--r-- | 459 | EQF_INTRO.hlp |
|
- | rw-r--r-- | 410 | EQT_ELIM.hlp |
|
- | rw-r--r-- | 335 | EQT_INTRO.hlp |
|
- | rw-r--r-- | 822 | EQ_IMP_RULE.hlp |
|
- | rw-r--r-- | 983 | EQ_MP.hlp |
|
- | rw-r--r-- | 590 | EQ_TAC.hlp |
|
- | rw-r--r-- | 677 | ETA_CONV.hlp |
|
- | rw-r--r-- | 829 | EVERY.hlp |
|
- | rw-r--r-- | 887 | EVERY_ASSUM.hlp |
|
- | rw-r--r-- | 934 | EVERY_CONV.hlp |
|
- | rw-r--r-- | 801 | EVERY_TCL.hlp |
|
- | rw-r--r-- | 656 | EXISTENCE.hlp |
|
- | rw-r--r-- | 994 | EXISTS_EQUATION.hlp |
|
- | rw-r--r-- | 870 | EXISTS_TAC.hlp |
|
- | rw-r--r-- | 981 | EXISTS_UPPERCASE.hlp |
|
- | rw-r--r-- | 940 | EXPAND_CASES_CONV.hlp |
|
- | rw-r--r-- | 1,047 | EXPAND_NSUM_CONV.hlp |
|
- | rw-r--r-- | 1,027 | EXPAND_SUM_CONV.hlp |
|
- | rw-r--r-- | 781 | EXPAND_TAC.hlp |
|
- | rw-r--r-- | 1,008 | FAIL_TAC.hlp |
|
- | rw-r--r-- | 1,727 | FIND_ASSUM.hlp |
|
- | rw-r--r-- | 696 | FIRST.hlp |
|
- | rw-r--r-- | 1,255 | FIRST_ASSUM.hlp |
|
- | rw-r--r-- | 714 | FIRST_CONV.hlp |
|
- | rw-r--r-- | 720 | FIRST_TCL.hlp |
|
- | rw-r--r-- | 1,169 | FIRST_X_ASSUM.hlp |
|
- | rw-r--r-- | 1,779 | FIX_TAC.hlp |
|
- | rw-r--r-- | 1,057 | FORALL_UNWIND_CONV.hlp |
|
- | rw-r--r-- | 1,210 | FREEZE_THEN.hlp |
|
- | rw-r--r-- | 276 | F_F.hlp |
|
- | rw-r--r-- | 1,035 | GABS_CONV.hlp |
|
- | rw-r--r-- | 1,012 | GEN.hlp |
|
- | rw-r--r-- | 729 | GENERAL_REWRITE_CONV.hlp |
|
- | rw-r--r-- | 935 | GENL.hlp |
|
- | rw-r--r-- | 744 | GEN_ALL.hlp |
|
- | rw-r--r-- | 899 | GEN_ALPHA_CONV.hlp |
|
- | rw-r--r-- | 1,174 | GEN_BETA_CONV.hlp |
|
- | rw-r--r-- | 1,454 | GEN_MESON_TAC.hlp |
|
- | rw-r--r-- | 1,784 | GEN_NNF_CONV.hlp |
|
- | rw-r--r-- | 1,519 | GEN_PART_MATCH.hlp |
|
- | rw-r--r-- | 2,222 | GEN_REAL_ARITH.hlp |
|
- | rw-r--r-- | 2,723 | GEN_REWRITE_CONV.hlp |
|
- | rw-r--r-- | 2,822 | GEN_REWRITE_RULE.hlp |
|
- | rw-r--r-- | 3,170 | GEN_REWRITE_TAC.hlp |
|
- | rw-r--r-- | 602 | GEN_SIMPLIFY_CONV.hlp |
|
- | rw-r--r-- | 803 | GEN_TAC.hlp |
|
- | rw-r--r-- | 819 | GSYM.hlp |
|
- | rw-r--r-- | 682 | HAS_SIZE_CONV.hlp |
|
- | rw-r--r-- | 794 | HAS_SIZE_DIMINDEX_RULE.hlp |
|
- | rw-r--r-- | 2,175 | HIGHER_REWRITE_CONV.hlp |
|
- | rw-r--r-- | 1,870 | HINT_EXISTS_TAC.hlp |
|
- | rw-r--r-- | 1,826 | HYP_TAC.hlp |
|
- | rw-r--r-- | 1,467 | HYP_UPPERCASE.hlp |
|
- | rw-r--r-- | 174 | I.hlp |
|
- | rw-r--r-- | 880 | IMP_ANTISYM_RULE.hlp |
|
- | rw-r--r-- | 3,854 | IMP_RES_THEN.hlp |
|
- | rw-r--r-- | 4,794 | IMP_REWRITE_TAC.hlp |
|
- | rw-r--r-- | 1,067 | IMP_REWR_CONV.hlp |
|
- | rw-r--r-- | 876 | IMP_TRANS.hlp |
|
- | rw-r--r-- | 1,870 | INDUCT_TAC.hlp |
|
- | rw-r--r-- | 886 | INSTANTIATE_ALL.hlp |
|
- | rw-r--r-- | 1,101 | INSTANTIATE_UPPERCASE.hlp |
|
- | rw-r--r-- | 1,261 | INST_TYPE.hlp |
|
- | rw-r--r-- | 1,616 | INST_UPPERCASE.hlp |
|
- | rw-r--r-- | 1,989 | INTEGER_RULE.hlp |
|
- | rw-r--r-- | 1,237 | INTEGER_TAC.hlp |
|
- | rw-r--r-- | 2,184 | INTRO_TAC.hlp |
|
- | rw-r--r-- | 740 | INT_ABS_CONV.hlp |
|
- | rw-r--r-- | 716 | INT_ADD_CONV.hlp |
|
- | rw-r--r-- | 853 | INT_ARITH.hlp |
|
- | rw-r--r-- | 1,372 | INT_ARITH_TAC.hlp |
|
- | rw-r--r-- | 952 | INT_EQ_CONV.hlp |
|
- | rw-r--r-- | 657 | INT_GE_CONV.hlp |
|
- | rw-r--r-- | 651 | INT_GT_CONV.hlp |
|
- | rw-r--r-- | 661 | INT_LE_CONV.hlp |
|
- | rw-r--r-- | 897 | INT_LT_CONV.hlp |
|
- | rw-r--r-- | 754 | INT_MAX_CONV.hlp |
|
- | rw-r--r-- | 754 | INT_MIN_CONV.hlp |
|
- | rw-r--r-- | 726 | INT_MUL_CONV.hlp |
|
- | rw-r--r-- | 958 | INT_NEG_CONV.hlp |
|
- | rw-r--r-- | 1,388 | INT_OF_REAL_THM.hlp |
|
- | rw-r--r-- | 1,940 | INT_POLY_CONV.hlp |
|
- | rw-r--r-- | 790 | INT_POW_CONV.hlp |
|
- | rw-r--r-- | 1,245 | INT_REDUCE_CONV.hlp |
|
- | rw-r--r-- | 1,333 | INT_RED_CONV.hlp |
|
- | rw-r--r-- | 803 | INT_REM_DOWN_CONV.hlp |
|
- | rw-r--r-- | 2,900 | INT_RING.hlp |
|
- | rw-r--r-- | 704 | INT_SGN_CONV.hlp |
|
- | rw-r--r-- | 724 | INT_SUB_CONV.hlp |
|
- | rw-r--r-- | 926 | ISPEC.hlp |
|
- | rw-r--r-- | 962 | ISPECL.hlp |
|
- | rw-r--r-- | 1,380 | ITAUT.hlp |
|
- | rw-r--r-- | 1,668 | ITAUT_TAC.hlp |
|
- | rw-r--r-- | 182 | K.hlp |
|
- | rw-r--r-- | 3,047 | LABEL_TAC.hlp |
|
- | rw-r--r-- | 920 | LAMBDA_ELIM_CONV.hlp |
|
- | rw-r--r-- | 562 | LAND_CONV.hlp |
|
- | rw-r--r-- | 1,298 | LEANCOP.hlp |
|
- | rw-r--r-- | 1,007 | LEANCOP_TAC.hlp |
|
- | rw-r--r-- | 737 | LENGTH_CONV.hlp |
|
- | rw-r--r-- | 1,035 | LET_TAC.hlp |
|
- | rw-r--r-- | 759 | LE_IMP.hlp |
|
- | rw-r--r-- | 701 | LIST_CONV.hlp |
|
- | rw-r--r-- | 3,021 | LIST_INDUCT_TAC.hlp |
|
- | rw-r--r-- | 817 | LIST_OF_SEQ_CONV.hlp |
|
- | rw-r--r-- | 1,042 | MAP_EVERY.hlp |
|
- | rw-r--r-- | 2,317 | MAP_FIRST.hlp |
|
- | rw-r--r-- | 957 | MATCH_ACCEPT_TAC.hlp |
|
- | rw-r--r-- | 2,502 | MATCH_CONV.hlp |
|
- | rw-r--r-- | 1,884 | MATCH_MP.hlp |
|
- | rw-r--r-- | 1,574 | MATCH_MP_TAC.hlp |
|
- | rw-r--r-- | 1,925 | MESON.hlp |
|
- | rw-r--r-- | 2,885 | MESON_TAC.hlp |
|
- | rw-r--r-- | 945 | META_EXISTS_TAC.hlp |
|
- | rw-r--r-- | 970 | META_SPEC_TAC.hlp |
|
- | rw-r--r-- | 1,343 | METIS.hlp |
|
- | rw-r--r-- | 1,832 | METIS_TAC.hlp |
|
- | rw-r--r-- | 678 | MK_BINOP_UPPERCASE.hlp |
|
- | rw-r--r-- | 641 | MK_COMB_TAC.hlp |
|
- | rw-r--r-- | 1,257 | MK_COMB_UPPERCASE.hlp |
|
- | rw-r--r-- | 829 | MK_CONJ_UPPERCASE.hlp |
|
- | rw-r--r-- | 859 | MK_DISJ_UPPERCASE.hlp |
|
- | rw-r--r-- | 918 | MK_EXISTS_UPPERCASE.hlp |
|
- | rw-r--r-- | 914 | MK_FORALL_UPPERCASE.hlp |
|
- | rw-r--r-- | 782 | MOD_DOWN_CONV.hlp |
|
- | rw-r--r-- | 881 | MONO_TAC.hlp |
|
- | rw-r--r-- | 763 | MP.hlp |
|
- | rw-r--r-- | 1,141 | MP_CONV.hlp |
|
- | rw-r--r-- | 656 | MP_TAC.hlp |
|
- | rw-r--r-- | 981 | NAME_ASSUMS_TAC.hlp |
|
- | rw-r--r-- | 1,298 | NANOCOP.hlp |
|
- | rw-r--r-- | 1,007 | NANOCOP_TAC.hlp |
|
- | rw-r--r-- | 1,422 | NNFC_CONV.hlp |
|
- | rw-r--r-- | 1,381 | NNF_CONV.hlp |
|
- | rw-r--r-- | 556 | NOT_ELIM.hlp |
|
- | rw-r--r-- | 573 | NOT_INTRO.hlp |
|
- | rw-r--r-- | 164 | NO_CONV.hlp |
|
- | rw-r--r-- | 1,128 | NO_TAC.hlp |
|
- | rw-r--r-- | 483 | NO_THEN.hlp |
|
- | rw-r--r-- | 1,137 | NUMBER_RULE.hlp |
|
- | rw-r--r-- | 1,372 | NUMBER_TAC.hlp |
|
- | rw-r--r-- | 710 | NUMSEG_CONV.hlp |
|
- | rw-r--r-- | 887 | NUM_ADD_CONV.hlp |
|
- | rw-r--r-- | 1,160 | NUM_CANCEL_CONV.hlp |
|
- | rw-r--r-- | 1,282 | NUM_DIV_CONV.hlp |
|
- | rw-r--r-- | 1,038 | NUM_EQ_CONV.hlp |
|
- | rw-r--r-- | 934 | NUM_EVEN_CONV.hlp |
|
- | rw-r--r-- | 1,142 | NUM_EXP_CONV.hlp |
|
- | rw-r--r-- | 1,032 | NUM_FACT_CONV.hlp |
|
- | rw-r--r-- | 1,072 | NUM_GE_CONV.hlp |
|
- | rw-r--r-- | 1,036 | NUM_GT_CONV.hlp |
|
- | rw-r--r-- | 1,078 | NUM_LE_CONV.hlp |
|
- | rw-r--r-- | 1,034 | NUM_LT_CONV.hlp |
|
- | rw-r--r-- | 890 | NUM_MAX_CONV.hlp |
|
- | rw-r--r-- | 890 | NUM_MIN_CONV.hlp |
|
- | rw-r--r-- | 1,313 | NUM_MOD_CONV.hlp |
|
- | rw-r--r-- | 916 | NUM_MULT_CONV.hlp |
|
- | rw-r--r-- | 1,200 | NUM_NORMALIZE_CONV.hlp |
|
- | rw-r--r-- | 920 | NUM_ODD_CONV.hlp |
|
- | rw-r--r-- | 1,031 | NUM_PRE_CONV.hlp |
|
- | rw-r--r-- | 1,559 | NUM_REDUCE_CONV.hlp |
|
- | rw-r--r-- | 1,300 | NUM_REDUCE_TAC.hlp |
|
- | rw-r--r-- | 1,873 | NUM_RED_CONV.hlp |
|
- | rw-r--r-- | 1,295 | NUM_REL_CONV.hlp |
|
- | rw-r--r-- | 1,925 | NUM_RING.hlp |
|
- | rw-r--r-- | 1,408 | NUM_SIMPLIFY_CONV.hlp |
|
- | rw-r--r-- | 1,275 | NUM_SUB_CONV.hlp |
|
- | rw-r--r-- | 985 | NUM_SUC_CONV.hlp |
|
- | rw-r--r-- | 903 | NUM_TO_INT_CONV.hlp |
|
- | rw-r--r-- | 1,028 | ONCE_ASM_REWRITE_RULE.hlp |
|
- | rw-r--r-- | 1,806 | ONCE_ASM_REWRITE_TAC.hlp |
|
- | rw-r--r-- | 832 | ONCE_ASM_SIMP_TAC.hlp |
|
- | rw-r--r-- | 2,358 | ONCE_DEPTH_CONV.hlp |
|
- | rw-r--r-- | 600 | ONCE_DEPTH_SQCONV.hlp |
|
- | rw-r--r-- | 797 | ONCE_REWRITE_CONV.hlp |
|
- | rw-r--r-- | 855 | ONCE_REWRITE_RULE.hlp |
|
- | rw-r--r-- | 1,830 | ONCE_REWRITE_TAC.hlp |
|
- | rw-r--r-- | 903 | ONCE_SIMPLIFY_CONV.hlp |
|
- | rw-r--r-- | 776 | ONCE_SIMP_CONV.hlp |
|
- | rw-r--r-- | 774 | ONCE_SIMP_RULE.hlp |
|
- | rw-r--r-- | 963 | ONCE_SIMP_TAC.hlp |
|
- | rw-r--r-- | 1,287 | ORDERED_IMP_REWR_CONV.hlp |
|
- | rw-r--r-- | 1,816 | ORDERED_REWR_CONV.hlp |
|
- | rw-r--r-- | 1,194 | ORELSE.hlp |
|
- | rw-r--r-- | 667 | ORELSEC.hlp |
|
- | rw-r--r-- | 586 | ORELSE_TCL.hlp |
|
- | rw-r--r-- | 2,111 | PART_MATCH.hlp |
|
- | rw-r--r-- | 1,056 | PATH_CONV.hlp |
|
- | rw-r--r-- | 1,232 | PAT_CONV.hlp |
|
- | rw-r--r-- | 1,322 | PINST.hlp |
|
- | rw-r--r-- | 2,421 | POP_ASSUM.hlp |
|
- | rw-r--r-- | 1,301 | POP_ASSUM_LIST.hlp |
|
- | rw-r--r-- | 758 | PRENEX_CONV.hlp |
|
- | rw-r--r-- | 931 | PRESIMP_CONV.hlp |
|
- | rw-r--r-- | 311 | PRINT_GOAL_TAC.hlp |
|
- | rw-r--r-- | 269 | PRINT_TERM_CONV.hlp |
|
- | rw-r--r-- | 1,351 | PROP_ATOM_CONV.hlp |
|
- | rw-r--r-- | 1,103 | PROVE_HYP.hlp |
|
- | rw-r--r-- | 853 | PURE_ASM_REWRITE_RULE.hlp |
|
- | rw-r--r-- | 948 | PURE_ASM_REWRITE_TAC.hlp |
|
- | rw-r--r-- | 733 | PURE_ASM_SIMP_TAC.hlp |
|
- | rw-r--r-- | 718 | PURE_ONCE_ASM_REWRITE_RULE.hlp |
|
- | rw-r--r-- | 1,050 | PURE_ONCE_ASM_REWRITE_TAC.hlp |
|
- | rw-r--r-- | 687 | PURE_ONCE_REWRITE_CONV.hlp |
|
- | rw-r--r-- | 711 | PURE_ONCE_REWRITE_RULE.hlp |
|
- | rw-r--r-- | 1,004 | PURE_ONCE_REWRITE_TAC.hlp |
|
- | rw-r--r-- | 774 | PURE_REWRITE_CONV.hlp |
|
- | rw-r--r-- | 904 | PURE_REWRITE_RULE.hlp |
|
- | rw-r--r-- | 1,799 | PURE_REWRITE_TAC.hlp |
|
- | rw-r--r-- | 708 | PURE_SIMP_CONV.hlp |
|
- | rw-r--r-- | 744 | PURE_SIMP_RULE.hlp |
|
- | rw-r--r-- | 826 | PURE_SIMP_TAC.hlp |
|
- | rw-r--r-- | 954 | RAND_CONV.hlp |
|
- | rw-r--r-- | 988 | RATOR_CONV.hlp |
|
- | rw-r--r-- | 2,057 | REAL_ARITH.hlp |
|
- | rw-r--r-- | 1,620 | REAL_ARITH_TAC.hlp |
|
- | rw-r--r-- | 1,481 | REAL_FIELD.hlp |
|
- | rw-r--r-- | 993 | REAL_IDEAL_CONV.hlp |
|
- | rw-r--r-- | 1,019 | REAL_INT_ABS_CONV.hlp |
|
- | rw-r--r-- | 995 | REAL_INT_ADD_CONV.hlp |
|
- | rw-r--r-- | 998 | REAL_INT_EQ_CONV.hlp |
|
- | rw-r--r-- | 934 | REAL_INT_GE_CONV.hlp |
|
- | rw-r--r-- | 928 | REAL_INT_GT_CONV.hlp |
|
- | rw-r--r-- | 938 | REAL_INT_LE_CONV.hlp |
|
- | rw-r--r-- | 938 | REAL_INT_LT_CONV.hlp |
|
- | rw-r--r-- | 1,005 | REAL_INT_MUL_CONV.hlp |
|
- | rw-r--r-- | 1,000 | REAL_INT_NEG_CONV.hlp |
|
- | rw-r--r-- | 1,074 | REAL_INT_POW_CONV.hlp |
|
- | rw-r--r-- | 797 | REAL_INT_RAT_CONV.hlp |
|
- | rw-r--r-- | 1,288 | REAL_INT_REDUCE_CONV.hlp |
|
- | rw-r--r-- | 1,390 | REAL_INT_RED_CONV.hlp |
|
- | rw-r--r-- | 1,003 | REAL_INT_SUB_CONV.hlp |
|
- | rw-r--r-- | 811 | REAL_LET_IMP.hlp |
|
- | rw-r--r-- | 767 | REAL_LE_IMP.hlp |
|
- | rw-r--r-- | 2,294 | REAL_LINEAR_PROVER.hlp |
|
- | rw-r--r-- | 1,225 | REAL_POLY_ADD_CONV.hlp |
|
- | rw-r--r-- | 2,425 | REAL_POLY_CONV.hlp |
|
- | rw-r--r-- | 1,227 | REAL_POLY_MUL_CONV.hlp |
|
- | rw-r--r-- | 1,169 | REAL_POLY_NEG_CONV.hlp |
|
- | rw-r--r-- | 1,238 | REAL_POLY_POW_CONV.hlp |
|
- | rw-r--r-- | 1,232 | REAL_POLY_SUB_CONV.hlp |
|
- | rw-r--r-- | 1,287 | REAL_RAT_ABS_CONV.hlp |
|
- | rw-r--r-- | 1,237 | REAL_RAT_ADD_CONV.hlp |
|
- | rw-r--r-- | 1,268 | REAL_RAT_DIV_CONV.hlp |
|
- | rw-r--r-- | 1,135 | REAL_RAT_EQ_CONV.hlp |
|
- | rw-r--r-- | 1,072 | REAL_RAT_GE_CONV.hlp |
|
- | rw-r--r-- | 1,054 | REAL_RAT_GT_CONV.hlp |
|
- | rw-r--r-- | 1,334 | REAL_RAT_INV_CONV.hlp |
|
- | rw-r--r-- | 1,072 | REAL_RAT_LE_CONV.hlp |
|
- | rw-r--r-- | 1,072 | REAL_RAT_LT_CONV.hlp |
|
- | rw-r--r-- | 1,245 | REAL_RAT_MAX_CONV.hlp |
|
- | rw-r--r-- | 1,242 | REAL_RAT_MIN_CONV.hlp |
|
- | rw-r--r-- | 1,360 | REAL_RAT_MUL_CONV.hlp |
|
- | rw-r--r-- | 1,233 | REAL_RAT_NEG_CONV.hlp |
|
- | rw-r--r-- | 1,283 | REAL_RAT_POW_CONV.hlp |
|
- | rw-r--r-- | 1,582 | REAL_RAT_REDUCE_CONV.hlp |
|
- | rw-r--r-- | 1,875 | REAL_RAT_RED_CONV.hlp |
|
- | rw-r--r-- | 1,177 | REAL_RAT_SGN_CONV.hlp |
|
- | rw-r--r-- | 1,278 | REAL_RAT_SUB_CONV.hlp |
|
- | rw-r--r-- | 3,224 | REAL_RING.hlp |
|
- | rw-r--r-- | 852 | RECALL_ACCEPT_TAC.hlp |
|
- | rw-r--r-- | 1,796 | REDEPTH_CONV.hlp |
|
- | rw-r--r-- | 567 | REDEPTH_SQCONV.hlp |
|
- | rw-r--r-- | 452 | REFL.hlp |
|
- | rw-r--r-- | 477 | REFL_TAC.hlp |
|
- | rw-r--r-- | 1,283 | REFUTE_THEN.hlp |
|
- | rw-r--r-- | 343 | REMARK_TAC.hlp |
|
- | rw-r--r-- | 671 | REMOVE_THEN.hlp |
|
- | rw-r--r-- | 964 | REPEATC.hlp |
|
- | rw-r--r-- | 839 | REPEAT_GTCL.hlp |
|
- | rw-r--r-- | 1,314 | REPEAT_TCL.hlp |
|
- | rw-r--r-- | 1,120 | REPEAT_UPPERCASE.hlp |
|
- | rw-r--r-- | 603 | REPLICATE_TAC.hlp |
|
- | rw-r--r-- | 707 | REVERSE_CONV.hlp |
|
- | rw-r--r-- | 973 | REWRITES_CONV.hlp |
|
- | rw-r--r-- | 1,639 | REWRITE_CONV.hlp |
|
- | rw-r--r-- | 1,825 | REWRITE_RULE.hlp |
|
- | rw-r--r-- | 3,729 | REWRITE_TAC.hlp |
|
- | rw-r--r-- | 5,760 | REWR_CONV.hlp |
|
- | rw-r--r-- | 712 | RIGHT_BETAS.hlp |
|
- | rw-r--r-- | 4,085 | RING.hlp |
|
- | rw-r--r-- | 823 | RING_AND_IDEAL_CONV.hlp |
|
- | rw-r--r-- | 805 | RULE_ASSUM_TAC.hlp |
|
- | rw-r--r-- | 1,478 | SELECT_CONV.hlp |
|
- | rw-r--r-- | 1,295 | SELECT_ELIM_TAC.hlp |
|
- | rw-r--r-- | 1,050 | SELECT_RULE.hlp |
|
- | rw-r--r-- | 4,238 | SEMIRING_NORMALIZERS_CONV.hlp |
|
- | rw-r--r-- | 2,202 | SEQ_IMP_REWRITE_TAC.hlp |
|
- | rw-r--r-- | 838 | SET_RULE.hlp |
|
- | rw-r--r-- | 845 | SET_TAC.hlp |
|
- | rw-r--r-- | 878 | SIMPLE_CHOOSE.hlp |
|
- | rw-r--r-- | 1,184 | SIMPLE_DISJ_CASES.hlp |
|
- | rw-r--r-- | 774 | SIMPLE_EXISTS.hlp |
|
- | rw-r--r-- | 882 | SIMPLIFY_CONV.hlp |
|
- | rw-r--r-- | 2,163 | SIMP_CONV.hlp |
|
- | rw-r--r-- | 614 | SIMP_RULE.hlp |
|
- | rw-r--r-- | 766 | SIMP_TAC.hlp |
|
- | rw-r--r-- | 1,439 | SKOLEM_CONV.hlp |
|
- | rw-r--r-- | 1,217 | SPEC.hlp |
|
- | rw-r--r-- | 1,422 | SPECL.hlp |
|
- | rw-r--r-- | 983 | SPEC_ALL.hlp |
|
- | rw-r--r-- | 665 | SPEC_TAC.hlp |
|
- | rw-r--r-- | 844 | SPEC_VAR.hlp |
|
- | rw-r--r-- | 839 | STRING_EQ_CONV.hlp |
|
- | rw-r--r-- | 2,345 | STRIP_ASSUME_TAC.hlp |
|
- | rw-r--r-- | 2,005 | STRIP_GOAL_THEN.hlp |
|
- | rw-r--r-- | 2,072 | STRIP_TAC.hlp |
|
- | rw-r--r-- | 2,322 | STRIP_THM_THEN.hlp |
|
- | rw-r--r-- | 1,915 | STRUCT_CASES_TAC.hlp |
|
- | rw-r--r-- | 1,682 | STRUCT_CASES_THEN.hlp |
|
- | rw-r--r-- | 1,163 | SUBGOAL_TAC.hlp |
|
- | rw-r--r-- | 3,834 | SUBGOAL_THEN.hlp |
|
- | rw-r--r-- | 1,055 | SUBLET_CONV.hlp |
|
- | rw-r--r-- | 2,001 | SUBS.hlp |
|
- | rw-r--r-- | 2,039 | SUBST1_TAC.hlp |
|
- | rw-r--r-- | 2,087 | SUBST_ALL_TAC.hlp |
|
- | rw-r--r-- | 1,073 | SUBST_VAR_TAC.hlp |
|
- | rw-r--r-- | 1,207 | SUBS_CONV.hlp |
|
- | rw-r--r-- | 1,553 | SUB_CONV.hlp |
|
- | rw-r--r-- | 737 | SYM.hlp |
|
- | rw-r--r-- | 452 | SYM_CONV.hlp |
|
- | rw-r--r-- | 620 | TAC_PROOF.hlp |
|
- | rw-r--r-- | 4,848 | TARGET_REWRITE_TAC.hlp |
|
- | rw-r--r-- | 1,464 | TAUT.hlp |
|
- | rw-r--r-- | 2,067 | THEN.hlp |
|
- | rw-r--r-- | 1,043 | THENC.hlp |
|
- | rw-r--r-- | 2,004 | THENL.hlp |
|
- | rw-r--r-- | 575 | THEN_TCL.hlp |
|
- | rw-r--r-- | 1,984 | TOP_DEPTH_CONV.hlp |
|
- | rw-r--r-- | 573 | TOP_DEPTH_SQCONV.hlp |
|
- | rw-r--r-- | 1,015 | TOP_SWEEP_CONV.hlp |
|
- | rw-r--r-- | 647 | TOP_SWEEP_SQCONV.hlp |
|
- | rw-r--r-- | 1,295 | TRANS.hlp |
|
- | rw-r--r-- | 1,606 | TRANS_TAC.hlp |
|
- | rw-r--r-- | 1,077 | TRY.hlp |
|
- | rw-r--r-- | 530 | TRY_CONV.hlp |
|
- | rw-r--r-- | 476 | UNDISCH.hlp |
|
- | rw-r--r-- | 646 | UNDISCH_ALL.hlp |
|
- | rw-r--r-- | 491 | UNDISCH_TAC.hlp |
|
- | rw-r--r-- | 668 | UNDISCH_THEN.hlp |
|
- | rw-r--r-- | 2,043 | UNIFY_ACCEPT_TAC.hlp |
|
- | rw-r--r-- | 948 | UNWIND_CONV.hlp |
|
- | rw-r--r-- | 559 | USE_THEN.hlp |
|
- | rw-r--r-- | 1,282 | VALID.hlp |
|
- | rw-r--r-- | 203 | W.hlp |
|
- | rw-r--r-- | 1,102 | WEAK_CNF_CONV.hlp |
|
- | rw-r--r-- | 1,021 | WEAK_DNF_CONV.hlp |
|
- | rw-r--r-- | 1,865 | WF_INDUCT_TAC.hlp |
|
- | rw-r--r-- | 1,397 | X_CHOOSE_TAC.hlp |
|
- | rw-r--r-- | 2,115 | X_CHOOSE_THEN.hlp |
|
- | rw-r--r-- | 911 | X_GEN_TAC.hlp |
|
- | rw-r--r-- | 971 | X_META_EXISTS_TAC.hlp |
|
- | rw-r--r-- | 924 | a.hlp |
|
- | rw-r--r-- | 977 | aconv.hlp |
|
- | rw-r--r-- | 510 | allpairs.hlp |
|
- | rw-r--r-- | 674 | alpha.hlp |
|
- | rw-r--r-- | 1,075 | alphaorder.hlp |
|
- | rw-r--r-- | 753 | apply.hlp |
|
- | rw-r--r-- | 1,264 | apply_prover.hlp |
|
- | rw-r--r-- | 934 | applyd.hlp |
|
- | rw-r--r-- | 502 | assoc.hlp |
|
- | rw-r--r-- | 655 | assocd.hlp |
|
- | rw-r--r-- | 1,035 | atleast.hlp |
|
- | rw-r--r-- | 824 | atoms.hlp |
|
- | rw-r--r-- | 408 | aty.hlp |
|
- | rw-r--r-- | 1,263 | augment.hlp |
|
- | rw-r--r-- | 725 | axioms.hlp |
|
- | rw-r--r-- | 1,019 | b.hlp |
|
- | rw-r--r-- | 1,389 | basic_congs.hlp |
|
- | rw-r--r-- | 1,172 | basic_convs.hlp |
|
- | rw-r--r-- | 679 | basic_net.hlp |
|
- | rw-r--r-- | 846 | basic_prover.hlp |
|
- | rw-r--r-- | 721 | basic_rectype_net.hlp |
|
- | rw-r--r-- | 1,826 | basic_rewrites.hlp |
|
- | rw-r--r-- | 586 | basic_ss.hlp |
|
- | rw-r--r-- | 580 | binders.hlp |
|
- | rw-r--r-- | 736 | binops.hlp |
|
- | rw-r--r-- | 294 | bndvar.hlp |
|
- | rw-r--r-- | 280 | body.hlp |
|
- | rw-r--r-- | 347 | bool_ty.hlp |
|
- | rw-r--r-- | 408 | bty.hlp |
|
- | rw-r--r-- | 269 | butlast.hlp |
|
- | rw-r--r-- | 320 | by.hlp |
|
- | rw-r--r-- | 387 | can.hlp |
|
- | rw-r--r-- | 809 | cases.hlp |
|
- | rw-r--r-- | 609 | check.hlp |
|
- | rw-r--r-- | 855 | checkpoint.hlp |
|
- | rw-r--r-- | 1,015 | choose.hlp |
|
- | rw-r--r-- | 430 | chop_list.hlp |
|
- | rw-r--r-- | 1,838 | combine.hlp |
|
- | rw-r--r-- | 1,304 | comment_token.hlp |
|
- | rw-r--r-- | 737 | compose_insts.hlp |
|
- | rw-r--r-- | 410 | concl.hlp |
|
- | rw-r--r-- | 1,167 | conjuncts.hlp |
|
- | rw-r--r-- | 307 | constants.hlp |
|
- | rw-r--r-- | 378 | copverb.hlp |
|
- | rw-r--r-- | 460 | current_goalstack.hlp |
|
- | rw-r--r-- | 453 | curry.hlp |
|
- | rw-r--r-- | 592 | decreasing.hlp |
|
- | rw-r--r-- | 973 | deep_alpha.hlp |
|
- | rw-r--r-- | 3,265 | define.hlp |
|
- | rw-r--r-- | 2,741 | define_quotient_type.hlp |
|
- | rw-r--r-- | 6,117 | define_type.hlp |
|
- | rw-r--r-- | 701 | define_type_raw.hlp |
|
- | rw-r--r-- | 845 | defined.hlp |
|
- | rw-r--r-- | 955 | definitions.hlp |
|
- | rw-r--r-- | 480 | delete_parser.hlp |
|
- | rw-r--r-- | 717 | delete_user_color_printer.hlp |
|
- | rw-r--r-- | 811 | delete_user_printer.hlp |
|
- | rw-r--r-- | 621 | denominator.hlp |
|
- | rw-r--r-- | 2,394 | derive_nonschematic_inductive_relations.hlp |
|
- | rw-r--r-- | 2,583 | derive_strong_induction.hlp |
|
- | rw-r--r-- | 456 | dest_abs.hlp |
|
- | rw-r--r-- | 596 | dest_binary.hlp |
|
- | rw-r--r-- | 658 | dest_binder.hlp |
|
- | rw-r--r-- | 619 | dest_binop.hlp |
|
- | rw-r--r-- | 669 | dest_char.hlp |
|
- | rw-r--r-- | 671 | dest_comb.hlp |
|
- | rw-r--r-- | 373 | dest_cond.hlp |
|
- | rw-r--r-- | 259 | dest_conj.hlp |
|
- | rw-r--r-- | 483 | dest_cons.hlp |
|
- | rw-r--r-- | 477 | dest_const.hlp |
|
- | rw-r--r-- | 341 | dest_disj.hlp |
|
- | rw-r--r-- | 320 | dest_eq.hlp |
|
- | rw-r--r-- | 413 | dest_exists.hlp |
|
- | rw-r--r-- | 559 | dest_finty.hlp |
|
- | rw-r--r-- | 405 | dest_forall.hlp |
|
- | rw-r--r-- | 622 | dest_fun_ty.hlp |
|
- | rw-r--r-- | 930 | dest_gabs.hlp |
|
- | rw-r--r-- | 594 | dest_iff.hlp |
|
- | rw-r--r-- | 364 | dest_imp.hlp |
|
- | rw-r--r-- | 615 | dest_intconst.hlp |
|
- | rw-r--r-- | 593 | dest_let.hlp |
|
- | rw-r--r-- | 361 | dest_list.hlp |
|
- | rw-r--r-- | 286 | dest_neg.hlp |
|
- | rw-r--r-- | 867 | dest_numeral.hlp |
|
- | rw-r--r-- | 412 | dest_pair.hlp |
|
- | rw-r--r-- | 652 | dest_realintconst.hlp |
|
- | rw-r--r-- | 365 | dest_select.hlp |
|
- | rw-r--r-- | 715 | dest_setenum.hlp |
|
- | rw-r--r-- | 929 | dest_small_numeral.hlp |
|
- | rw-r--r-- | 512 | dest_string.hlp |
|
- | rw-r--r-- | 346 | dest_thm.hlp |
|
- | rw-r--r-- | 589 | dest_type.hlp |
|
- | rw-r--r-- | 386 | dest_uexists.hlp |
|
- | rw-r--r-- | 389 | dest_var.hlp |
|
- | rw-r--r-- | 472 | dest_vartype.hlp |
|
- | rw-r--r-- | 1,157 | disjuncts.hlp |
|
- | rw-r--r-- | 911 | distinctness.hlp |
|
- | rw-r--r-- | 446 | distinctness_store.hlp |
|
- | rw-r--r-- | 674 | do_list.hlp |
|
- | rw-r--r-- | 843 | dom.hlp |
|
- | rw-r--r-- | 238 | dpty.hlp |
|
- | rw-r--r-- | 1,648 | e.hlp |
|
- | rw-r--r-- | 390 | el.hlp |
|
- | rw-r--r-- | 1,301 | elistof.hlp |
|
- | rw-r--r-- | 696 | empty_net.hlp |
|
- | rw-r--r-- | 502 | empty_ss.hlp |
|
- | rw-r--r-- | 447 | end_itlist.hlp |
|
- | rw-r--r-- | 2,269 | enter.hlp |
|
- | rw-r--r-- | 556 | equals_goal.hlp |
|
- | rw-r--r-- | 517 | equals_thm.hlp |
|
- | rw-r--r-- | 2,056 | er.hlp |
|
- | rw-r--r-- | 253 | exactly.hlp |
|
- | rw-r--r-- | 567 | exists.hlp |
|
- | rw-r--r-- | 462 | explode.hlp |
|
- | rw-r--r-- | 1,281 | extend_basic_congs.hlp |
|
- | rw-r--r-- | 1,335 | extend_basic_convs.hlp |
|
- | rw-r--r-- | 608 | extend_basic_rewrites.hlp |
|
- | rw-r--r-- | 902 | extend_rectype_net.hlp |
|
- | rw-r--r-- | 136 | f_f_.hlp |
|
- | rw-r--r-- | 652 | fail.hlp |
|
- | rw-r--r-- | 678 | file_of_string.hlp |
|
- | rw-r--r-- | 895 | file_on_path.hlp |
|
- | rw-r--r-- | 417 | filter.hlp |
|
- | rw-r--r-- | 431 | find.hlp |
|
- | rw-r--r-- | 406 | find_index.hlp |
|
- | rw-r--r-- | 811 | find_path.hlp |
|
- | rw-r--r-- | 449 | find_term.hlp |
|
- | rw-r--r-- | 598 | find_terms.hlp |
|
- | rw-r--r-- | 971 | finished.hlp |
|
- | rw-r--r-- | 1,052 | fix.hlp |
|
- | rw-r--r-- | 351 | flat.hlp |
|
- | rw-r--r-- | 497 | flush_goalstack.hlp |
|
- | rw-r--r-- | 1,377 | foldl.hlp |
|
- | rw-r--r-- | 1,424 | foldr.hlp |
|
- | rw-r--r-- | 760 | follow_path.hlp |
|
- | rw-r--r-- | 560 | forall.hlp |
|
- | rw-r--r-- | 724 | forall2.hlp |
|
- | rw-r--r-- | 897 | free_in.hlp |
|
- | rw-r--r-- | 560 | frees.hlp |
|
- | rw-r--r-- | 739 | freesin.hlp |
|
- | rw-r--r-- | 635 | freesl.hlp |
|
- | rw-r--r-- | 736 | funpow.hlp |
|
- | rw-r--r-- | 607 | g.hlp |
|
- | rw-r--r-- | 529 | gcd.hlp |
|
- | rw-r--r-- | 669 | gcd_num.hlp |
|
- | rw-r--r-- | 861 | genvar.hlp |
|
- | rw-r--r-- | 431 | get_const_type.hlp |
|
- | rw-r--r-- | 728 | get_infix_status.hlp |
|
- | rw-r--r-- | 607 | get_type_arity.hlp |
|
- | rw-r--r-- | 902 | graph.hlp |
|
- | rw-r--r-- | 213 | hd.hlp |
|
- | rw-r--r-- | 1,722 | help.hlp |
|
- | rw-r--r-- | 607 | help_path.hlp |
|
- | rw-r--r-- | 644 | hide_constant.hlp |
|
- | rw-r--r-- | 688 | hol_dir.hlp |
|
- | rw-r--r-- | 766 | hol_expand_directory.hlp |
|
- | rw-r--r-- | 318 | hol_version.hlp |
|
- | rw-r--r-- | 425 | hyp.hlp |
|
- | rw-r--r-- | 1,198 | ideal_cofactors.hlp |
|
- | rw-r--r-- | 946 | ignore_constant_varstruct.hlp |
|
- | rw-r--r-- | 544 | implode.hlp |
|
- | rw-r--r-- | 656 | increasing.hlp |
|
- | rw-r--r-- | 569 | index.hlp |
|
- | rw-r--r-- | 1,632 | inductive_type_store.hlp |
|
- | rw-r--r-- | 447 | infixes.hlp |
|
- | rw-r--r-- | 961 | injectivity.hlp |
|
- | rw-r--r-- | 448 | injectivity_store.hlp |
|
- | rw-r--r-- | 547 | insert.hlp |
|
- | rw-r--r-- | 768 | insert_prime.hlp |
|
- | rw-r--r-- | 1,361 | inst.hlp |
|
- | rw-r--r-- | 572 | inst_goal.hlp |
|
- | rw-r--r-- | 547 | install_parser.hlp |
|
- | rw-r--r-- | 1,317 | install_user_color_printer.hlp |
|
- | rw-r--r-- | 2,113 | install_user_printer.hlp |
|
- | rw-r--r-- | 489 | installed_parsers.hlp |
|
- | rw-r--r-- | 1,205 | instantiate.hlp |
|
- | rw-r--r-- | 1,754 | instantiate_casewise_recursion.hlp |
|
- | rw-r--r-- | 1,918 | int_ideal_cofactors.hlp |
|
- | rw-r--r-- | 655 | intersect.hlp |
|
- | rw-r--r-- | 402 | is_abs.hlp |
|
- | rw-r--r-- | 703 | is_binary.hlp |
|
- | rw-r--r-- | 705 | is_binder.hlp |
|
- | rw-r--r-- | 618 | is_binop.hlp |
|
- | rw-r--r-- | 412 | is_comb.hlp |
|
- | rw-r--r-- | 278 | is_cond.hlp |
|
- | rw-r--r-- | 266 | is_conj.hlp |
|
- | rw-r--r-- | 309 | is_cons.hlp |
|
- | rw-r--r-- | 595 | is_const.hlp |
|
- | rw-r--r-- | 266 | is_disj.hlp |
|
- | rw-r--r-- | 523 | is_eq.hlp |
|
- | rw-r--r-- | 307 | is_exists.hlp |
|
- | rw-r--r-- | 301 | is_forall.hlp |
|
- | rw-r--r-- | 695 | is_gabs.hlp |
|
- | rw-r--r-- | 607 | is_hidden.hlp |
|
- | rw-r--r-- | 646 | is_iff.hlp |
|
- | rw-r--r-- | 287 | is_imp.hlp |
|
- | rw-r--r-- | 559 | is_intconst.hlp |
|
- | rw-r--r-- | 451 | is_let.hlp |
|
- | rw-r--r-- | 281 | is_list.hlp |
|
- | rw-r--r-- | 265 | is_neg.hlp |
|
- | rw-r--r-- | 321 | is_numeral.hlp |
|
- | rw-r--r-- | 368 | is_pair.hlp |
|
- | rw-r--r-- | 421 | is_prefix.hlp |
|
- | rw-r--r-- | 720 | is_ratconst.hlp |
|
- | rw-r--r-- | 596 | is_realintconst.hlp |
|
- | rw-r--r-- | 456 | is_reserved_word.hlp |
|
- | rw-r--r-- | 280 | is_select.hlp |
|
- | rw-r--r-- | 544 | is_setenum.hlp |
|
- | rw-r--r-- | 492 | is_type.hlp |
|
- | rw-r--r-- | 341 | is_uexists.hlp |
|
- | rw-r--r-- | 838 | is_undefined.hlp |
|
- | rw-r--r-- | 380 | is_var.hlp |
|
- | rw-r--r-- | 466 | is_vartype.hlp |
|
- | rw-r--r-- | 430 | isalnum.hlp |
|
- | rw-r--r-- | 417 | isalpha.hlp |
|
- | rw-r--r-- | 421 | isbra.hlp |
|
- | rw-r--r-- | 348 | isnum.hlp |
|
- | rw-r--r-- | 365 | issep.hlp |
|
- | rw-r--r-- | 389 | isspace.hlp |
|
- | rw-r--r-- | 695 | issymb.hlp |
|
- | rw-r--r-- | 492 | it.hlp |
|
- | rw-r--r-- | 490 | itlist.hlp |
|
- | rw-r--r-- | 674 | itlist2.hlp |
|
- | rw-r--r-- | 222 | last.hlp |
|
- | rw-r--r-- | 551 | lcm_num.hlp |
|
- | rw-r--r-- | 1,545 | leftbin.hlp |
|
- | rw-r--r-- | 170 | length.hlp |
|
- | rw-r--r-- | 2,001 | let_CONV.hlp |
|
- | rw-r--r-- | 1,537 | lex.hlp |
|
- | rw-r--r-- | 953 | lhand.hlp |
|
- | rw-r--r-- | 301 | lhs.hlp |
|
- | rw-r--r-- | 4,542 | lift_function.hlp |
|
- | rw-r--r-- | 3,472 | lift_theorem.hlp |
|
- | rw-r--r-- | 413 | list_mk_abs.hlp |
|
- | rw-r--r-- | 1,040 | list_mk_binop.hlp |
|
- | rw-r--r-- | 708 | list_mk_comb.hlp |
|
- | rw-r--r-- | 571 | list_mk_conj.hlp |
|
- | rw-r--r-- | 580 | list_mk_disj.hlp |
|
- | rw-r--r-- | 812 | list_mk_exists.hlp |
|
- | rw-r--r-- | 564 | list_mk_forall.hlp |
|
- | rw-r--r-- | 523 | list_mk_gabs.hlp |
|
- | rw-r--r-- | 977 | list_mk_icomb.hlp |
|
- | rw-r--r-- | 1,277 | listof.hlp |
|
- | rw-r--r-- | 755 | load_on_path.hlp |
|
- | rw-r--r-- | 815 | load_path.hlp |
|
- | rw-r--r-- | 527 | loaded_files.hlp |
|
- | rw-r--r-- | 761 | loads.hlp |
|
- | rw-r--r-- | 1,100 | loadt.hlp |
|
- | rw-r--r-- | 2,685 | lookup.hlp |
|
- | rw-r--r-- | 621 | make_args.hlp |
|
- | rw-r--r-- | 1,399 | make_overloadable.hlp |
|
- | rw-r--r-- | 1,066 | many.hlp |
|
- | rw-r--r-- | 345 | map.hlp |
|
- | rw-r--r-- | 417 | map2.hlp |
|
- | rw-r--r-- | 940 | mapf.hlp |
|
- | rw-r--r-- | 682 | mapfilter.hlp |
|
- | rw-r--r-- | 314 | mem.hlp |
|
- | rw-r--r-- | 810 | mem_prime.hlp |
|
- | rw-r--r-- | 649 | merge.hlp |
|
- | rw-r--r-- | 1,116 | merge_nets.hlp |
|
- | rw-r--r-- | 727 | mergesort.hlp |
|
- | rw-r--r-- | 1,014 | meson_brand.hlp |
|
- | rw-r--r-- | 714 | meson_chatty.hlp |
|
- | rw-r--r-- | 768 | meson_dcutin.hlp |
|
- | rw-r--r-- | 811 | meson_depth.hlp |
|
- | rw-r--r-- | 912 | meson_prefine.hlp |
|
- | rw-r--r-- | 992 | meson_skew.hlp |
|
- | rw-r--r-- | 954 | meson_split_limit.hlp |
|
- | rw-r--r-- | 353 | metisverb.hlp |
|
- | rw-r--r-- | 475 | mk_abs.hlp |
|
- | rw-r--r-- | 824 | mk_binary.hlp |
|
- | rw-r--r-- | 737 | mk_binder.hlp |
|
- | rw-r--r-- | 655 | mk_binop.hlp |
|
- | rw-r--r-- | 578 | mk_char.hlp |
|
- | rw-r--r-- | 587 | mk_comb.hlp |
|
- | rw-r--r-- | 317 | mk_cond.hlp |
|
- | rw-r--r-- | 373 | mk_conj.hlp |
|
- | rw-r--r-- | 480 | mk_cons.hlp |
|
- | rw-r--r-- | 970 | mk_const.hlp |
|
- | rw-r--r-- | 359 | mk_disj.hlp |
|
- | rw-r--r-- | 298 | mk_eq.hlp |
|
- | rw-r--r-- | 408 | mk_exists.hlp |
|
- | rw-r--r-- | 500 | mk_finty.hlp |
|
- | rw-r--r-- | 616 | mk_flist.hlp |
|
- | rw-r--r-- | 406 | mk_forall.hlp |
|
- | rw-r--r-- | 818 | mk_fset.hlp |
|
- | rw-r--r-- | 787 | mk_fthm.hlp |
|
- | rw-r--r-- | 500 | mk_fun_ty.hlp |
|
- | rw-r--r-- | 1,346 | mk_gabs.hlp |
|
- | rw-r--r-- | 400 | mk_goalstate.hlp |
|
- | rw-r--r-- | 769 | mk_icomb.hlp |
|
- | rw-r--r-- | 522 | mk_iff.hlp |
|
- | rw-r--r-- | 351 | mk_imp.hlp |
|
- | rw-r--r-- | 727 | mk_intconst.hlp |
|
- | rw-r--r-- | 681 | mk_let.hlp |
|
- | rw-r--r-- | 711 | mk_list.hlp |
|
- | rw-r--r-- | 939 | mk_mconst.hlp |
|
- | rw-r--r-- | 332 | mk_neg.hlp |
|
- | rw-r--r-- | 771 | mk_numeral.hlp |
|
- | rw-r--r-- | 304 | mk_pair.hlp |
|
- | rw-r--r-- | 958 | mk_primed_var.hlp |
|
- | rw-r--r-- | 1,794 | mk_prover.hlp |
|
- | rw-r--r-- | 755 | mk_realintconst.hlp |
|
- | rw-r--r-- | 1,237 | mk_rewrites.hlp |
|
- | rw-r--r-- | 254 | mk_select.hlp |
|
- | rw-r--r-- | 840 | mk_setenum.hlp |
|
- | rw-r--r-- | 694 | mk_small_numeral.hlp |
|
- | rw-r--r-- | 480 | mk_string.hlp |
|
- | rw-r--r-- | 982 | mk_thm.hlp |
|
- | rw-r--r-- | 717 | mk_type.hlp |
|
- | rw-r--r-- | 411 | mk_uexists.hlp |
|
- | rw-r--r-- | 472 | mk_var.hlp |
|
- | rw-r--r-- | 738 | mk_vartype.hlp |
|
- | rw-r--r-- | 1,867 | monotonicity_theorems.hlp |
|
- | rw-r--r-- | 250 | name.hlp |
|
- | rw-r--r-- | 553 | name_of.hlp |
|
- | rw-r--r-- | 972 | needs.hlp |
|
- | rw-r--r-- | 786 | net_of_cong.hlp |
|
- | rw-r--r-- | 846 | net_of_conv.hlp |
|
- | rw-r--r-- | 1,219 | net_of_thm.hlp |
|
- | rw-r--r-- | 1,224 | new_axiom.hlp |
|
- | rw-r--r-- | 1,693 | new_basic_definition.hlp |
|
- | rw-r--r-- | 2,084 | new_basic_type_definition.hlp |
|
- | rw-r--r-- | 590 | new_constant.hlp |
|
- | rw-r--r-- | 1,652 | new_definition.hlp |
|
- | rw-r--r-- | 5,056 | new_inductive_definition.hlp |
|
- | rw-r--r-- | 3,462 | new_inductive_set.hlp |
|
- | rw-r--r-- | 3,202 | new_recursive_definition.hlp |
|
- | rw-r--r-- | 1,665 | new_specification.hlp |
|
- | rw-r--r-- | 964 | new_type.hlp |
|
- | rw-r--r-- | 955 | new_type_abbrev.hlp |
|
- | rw-r--r-- | 2,012 | new_type_definition.hlp |
|
- | rw-r--r-- | 937 | nothing.hlp |
|
- | rw-r--r-- | 583 | nsplit.hlp |
|
- | rw-r--r-- | 537 | null_inst.hlp |
|
- | rw-r--r-- | 485 | null_meta.hlp |
|
- | rw-r--r-- | 377 | num_0.hlp |
|
- | rw-r--r-- | 376 | num_1.hlp |
|
- | rw-r--r-- | 380 | num_10.hlp |
|
- | rw-r--r-- | 376 | num_2.hlp |
|
- | rw-r--r-- | 634 | num_CONV.hlp |
|
- | rw-r--r-- | 655 | num_of_string.hlp |
|
- | rw-r--r-- | 672 | numdom.hlp |
|
- | rw-r--r-- | 609 | numerator.hlp |
|
- | rw-r--r-- | 199 | o.hlp |
|
- | rw-r--r-- | 628 | occurs_in.hlp |
|
- | rw-r--r-- | 237 | omit.hlp |
|
- | rw-r--r-- | 128 | orelse_.hlp |
|
- | rw-r--r-- | 162 | orelse_tcl_.hlp |
|
- | rw-r--r-- | 126 | orelsec_.hlp |
|
- | rw-r--r-- | 2,106 | overload_interface.hlp |
|
- | rw-r--r-- | 2,029 | override_interface.hlp |
|
- | rw-r--r-- | 524 | p.hlp |
|
- | rw-r--r-- | 685 | parse_as_binder.hlp |
|
- | rw-r--r-- | 1,174 | parse_as_infix.hlp |
|
- | rw-r--r-- | 472 | parse_as_prefix.hlp |
|
- | rw-r--r-- | 756 | parse_inductive_type_specification.hlp |
|
- | rw-r--r-- | 602 | parse_preterm.hlp |
|
- | rw-r--r-- | 602 | parse_pretype.hlp |
|
- | rw-r--r-- | 765 | parse_term.hlp |
|
- | rw-r--r-- | 475 | parse_type.hlp |
|
- | rw-r--r-- | 548 | parses_as_binder.hlp |
|
- | rw-r--r-- | 499 | partition.hlp |
|
- | rw-r--r-- | 995 | possibly.hlp |
|
- | rw-r--r-- | 405 | pow10.hlp |
|
- | rw-r--r-- | 401 | pow2.hlp |
|
- | rw-r--r-- | 587 | pp_print_colored_qterm.hlp |
|
- | rw-r--r-- | 590 | pp_print_colored_qtype.hlp |
|
- | rw-r--r-- | 1,155 | pp_print_colored_term.hlp |
|
- | rw-r--r-- | 549 | pp_print_colored_thm.hlp |
|
- | rw-r--r-- | 922 | pp_print_colored_type.hlp |
|
- | rw-r--r-- | 610 | pp_print_fpf.hlp |
|
- | rw-r--r-- | 541 | pp_print_num.hlp |
|
- | rw-r--r-- | 587 | pp_print_qterm.hlp |
|
- | rw-r--r-- | 610 | pp_print_qtype.hlp |
|
- | rw-r--r-- | 593 | pp_print_term.hlp |
|
- | rw-r--r-- | 427 | pp_print_thm.hlp |
|
- | rw-r--r-- | 607 | pp_print_type.hlp |
|
- | rw-r--r-- | 883 | prebroken_binops.hlp |
|
- | rw-r--r-- | 604 | prefixes.hlp |
|
- | rw-r--r-- | 583 | preterm_of_term.hlp |
|
- | rw-r--r-- | 587 | pretype_of_type.hlp |
|
- | rw-r--r-- | 902 | print_all_thm.hlp |
|
- | rw-r--r-- | 463 | print_fpf.hlp |
|
- | rw-r--r-- | 402 | print_goal.hlp |
|
- | rw-r--r-- | 1,674 | print_goal_hyp_max_boxes.hlp |
|
- | rw-r--r-- | 434 | print_goalstack.hlp |
|
- | rw-r--r-- | 401 | print_num.hlp |
|
- | rw-r--r-- | 444 | print_qterm.hlp |
|
- | rw-r--r-- | 454 | print_qtype.hlp |
|
- | rw-r--r-- | 526 | print_term.hlp |
|
- | rw-r--r-- | 350 | print_thm.hlp |
|
- | rw-r--r-- | 777 | print_to_string.hlp |
|
- | rw-r--r-- | 532 | print_type.hlp |
|
- | rw-r--r-- | 1,832 | print_types_of_subterms.hlp |
|
- | rw-r--r-- | 1,517 | print_unambiguous_comprehensions.hlp |
|
- | rw-r--r-- | 1,617 | prioritize_int.hlp |
|
- | rw-r--r-- | 1,803 | prioritize_num.hlp |
|
- | rw-r--r-- | 1,779 | prioritize_overload.hlp |
|
- | rw-r--r-- | 1,628 | prioritize_real.hlp |
|
- | rw-r--r-- | 763 | prove.hlp |
|
- | rw-r--r-- | 1,512 | prove_cases_thm.hlp |
|
- | rw-r--r-- | 1,828 | prove_constructors_distinct.hlp |
|
- | rw-r--r-- | 1,927 | prove_constructors_injective.hlp |
|
- | rw-r--r-- | 3,197 | prove_general_recursive_function_exists.hlp |
|
- | rw-r--r-- | 2,374 | prove_inductive_relations_exist.hlp |
|
- | rw-r--r-- | 723 | prove_monotonicity_hyps.hlp |
|
- | rw-r--r-- | 3,540 | prove_recursive_functions_exist.hlp |
|
- | rw-r--r-- | 2,469 | pure_prove_recursive_function_exists.hlp |
|
- | rw-r--r-- | 1,543 | qmap.hlp |
|
- | rw-r--r-- | 571 | quotexpander.hlp |
|
- | rw-r--r-- | 1,012 | r.hlp |
|
- | rw-r--r-- | 811 | ran.hlp |
|
- | rw-r--r-- | 353 | rand.hlp |
|
- | rw-r--r-- | 739 | rat_of_term.hlp |
|
- | rw-r--r-- | 447 | rator.hlp |
|
- | rw-r--r-- | 1,910 | real_ideal_cofactors.hlp |
|
- | rw-r--r-- | 586 | reduce_interface.hlp |
|
- | rw-r--r-- | 558 | refine.hlp |
|
- | rw-r--r-- | 677 | remark.hlp |
|
- | rw-r--r-- | 418 | remove.hlp |
|
- | rw-r--r-- | 573 | remove_interface.hlp |
|
- | rw-r--r-- | 818 | remove_type_abbrev.hlp |
|
- | rw-r--r-- | 562 | repeat.hlp |
|
- | rw-r--r-- | 283 | replicate.hlp |
|
- | rw-r--r-- | 345 | report.hlp |
|
- | rw-r--r-- | 806 | report_timing.hlp |
|
- | rw-r--r-- | 537 | reserve_words.hlp |
|
- | rw-r--r-- | 637 | reserved_words.hlp |
|
- | rw-r--r-- | 737 | retypecheck.hlp |
|
- | rw-r--r-- | 172 | rev.hlp |
|
- | rw-r--r-- | 521 | rev_assoc.hlp |
|
- | rw-r--r-- | 679 | rev_assocd.hlp |
|
- | rw-r--r-- | 447 | rev_itlist.hlp |
|
- | rw-r--r-- | 704 | rev_itlist2.hlp |
|
- | rw-r--r-- | 695 | rev_splitlist.hlp |
|
- | rw-r--r-- | 1,335 | reverse_interface_mapping.hlp |
|
- | rw-r--r-- | 287 | rhs.hlp |
|
- | rw-r--r-- | 1,553 | rightbin.hlp |
|
- | rw-r--r-- | 359 | rotate.hlp |
|
- | rw-r--r-- | 2,540 | search.hlp |
|
- | rw-r--r-- | 2,351 | self_destruct.hlp |
|
- | rw-r--r-- | 725 | set_basic_congs.hlp |
|
- | rw-r--r-- | 942 | set_basic_convs.hlp |
|
- | rw-r--r-- | 740 | set_basic_rewrites.hlp |
|
- | rw-r--r-- | 448 | set_color_printer.hlp |
|
- | rw-r--r-- | 542 | set_eq.hlp |
|
- | rw-r--r-- | 1,976 | set_goal.hlp |
|
- | rw-r--r-- | 1,755 | set_verbose_symbols.hlp |
|
- | rw-r--r-- | 490 | setify.hlp |
|
- | rw-r--r-- | 702 | shareout.hlp |
|
- | rw-r--r-- | 964 | some.hlp |
|
- | rw-r--r-- | 1,900 | sort.hlp |
|
- | rw-r--r-- | 700 | splitlist.hlp |
|
- | rw-r--r-- | 834 | ss_of_congs.hlp |
|
- | rw-r--r-- | 858 | ss_of_conv.hlp |
|
- | rw-r--r-- | 930 | ss_of_maker.hlp |
|
- | rw-r--r-- | 895 | ss_of_prover.hlp |
|
- | rw-r--r-- | 795 | ss_of_provers.hlp |
|
- | rw-r--r-- | 847 | ss_of_thms.hlp |
|
- | rw-r--r-- | 694 | startup_banner.hlp |
|
- | rw-r--r-- | 655 | string_of_file.hlp |
|
- | rw-r--r-- | 604 | string_of_term.hlp |
|
- | rw-r--r-- | 834 | string_of_thm.hlp |
|
- | rw-r--r-- | 478 | string_of_type.hlp |
|
- | rw-r--r-- | 705 | strings_of_file.hlp |
|
- | rw-r--r-- | 500 | strip_abs.hlp |
|
- | rw-r--r-- | 588 | strip_comb.hlp |
|
- | rw-r--r-- | 436 | strip_exists.hlp |
|
- | rw-r--r-- | 431 | strip_forall.hlp |
|
- | rw-r--r-- | 709 | strip_gabs.hlp |
|
- | rw-r--r-- | 878 | strip_ncomb.hlp |
|
- | rw-r--r-- | 670 | striplist.hlp |
|
- | rw-r--r-- | 513 | subset.hlp |
|
- | rw-r--r-- | 1,180 | subst.hlp |
|
- | rw-r--r-- | 570 | subtract.hlp |
|
- | rw-r--r-- | 787 | subtract_prime.hlp |
|
- | rw-r--r-- | 388 | temp_path.hlp |
|
- | rw-r--r-- | 1,237 | term_match.hlp |
|
- | rw-r--r-- | 702 | term_of_preterm.hlp |
|
- | rw-r--r-- | 687 | term_of_rat.hlp |
|
- | rw-r--r-- | 1,079 | term_order.hlp |
|
- | rw-r--r-- | 768 | term_type_unify.hlp |
|
- | rw-r--r-- | 814 | term_unify.hlp |
|
- | rw-r--r-- | 1,913 | the_definitions.hlp |
|
- | rw-r--r-- | 1,784 | the_implicit_types.hlp |
|
- | rw-r--r-- | 1,286 | the_inductive_definitions.hlp |
|
- | rw-r--r-- | 423 | the_inductive_types.hlp |
|
- | rw-r--r-- | 552 | the_interface.hlp |
|
- | rw-r--r-- | 1,533 | the_overload_skeletons.hlp |
|
- | rw-r--r-- | 1,027 | the_specifications.hlp |
|
- | rw-r--r-- | 1,239 | the_type_definitions.hlp |
|
- | rw-r--r-- | 120 | then_.hlp |
|
- | rw-r--r-- | 154 | then_tcl_.hlp |
|
- | rw-r--r-- | 118 | thenc_.hlp |
|
- | rw-r--r-- | 129 | thenl_.hlp |
|
- | rw-r--r-- | 967 | theorems.hlp |
|
- | rw-r--r-- | 554 | thm_frees.hlp |
|
- | rw-r--r-- | 671 | time.hlp |
|
- | rw-r--r-- | 250 | tl.hlp |
|
- | rw-r--r-- | 613 | top_goal.hlp |
|
- | rw-r--r-- | 511 | top_realgoal.hlp |
|
- | rw-r--r-- | 790 | top_thm.hlp |
|
- | rw-r--r-- | 834 | try_user_color_printer.hlp |
|
- | rw-r--r-- | 533 | try_user_parser.hlp |
|
- | rw-r--r-- | 1,054 | try_user_printer.hlp |
|
- | rw-r--r-- | 904 | tryapplyd.hlp |
|
- | rw-r--r-- | 523 | tryfind.hlp |
|
- | rw-r--r-- | 361 | type_abbrevs.hlp |
|
- | rw-r--r-- | 1,489 | type_invention_error.hlp |
|
- | rw-r--r-- | 1,769 | type_invention_warning.hlp |
|
- | rw-r--r-- | 1,349 | type_match.hlp |
|
- | rw-r--r-- | 181 | type_of.hlp |
|
- | rw-r--r-- | 637 | type_of_pretype.hlp |
|
- | rw-r--r-- | 739 | type_subst.hlp |
|
- | rw-r--r-- | 590 | type_unify.hlp |
|
- | rw-r--r-- | 639 | type_vars_in_term.hlp |
|
- | rw-r--r-- | 713 | types.hlp |
|
- | rw-r--r-- | 1,170 | typify_universal_set.hlp |
|
- | rw-r--r-- | 793 | tysubst.hlp |
|
- | rw-r--r-- | 369 | tyvars.hlp |
|
- | rw-r--r-- | 323 | uncurry.hlp |
|
- | rw-r--r-- | 944 | undefine.hlp |
|
- | rw-r--r-- | 803 | undefined.hlp |
|
- | rw-r--r-- | 654 | unhide_constant.hlp |
|
- | rw-r--r-- | 570 | union.hlp |
|
- | rw-r--r-- | 834 | union_prime.hlp |
|
- | rw-r--r-- | 457 | unions.hlp |
|
- | rw-r--r-- | 683 | unions_prime.hlp |
|
- | rw-r--r-- | 445 | uniq.hlp |
|
- | rw-r--r-- | 833 | unparse_as_binder.hlp |
|
- | rw-r--r-- | 618 | unparse_as_infix.hlp |
|
- | rw-r--r-- | 502 | unparse_as_prefix.hlp |
|
- | rw-r--r-- | 714 | unreserve_words.hlp |
|
- | rw-r--r-- | 1,069 | unset_jrh_lexer.hlp |
|
- | rw-r--r-- | 1,629 | unset_then_multiple_subgoals.hlp |
|
- | rw-r--r-- | 1,043 | unset_verbose_symbols.hlp |
|
- | rw-r--r-- | 920 | unspaced_binops.hlp |
|
- | rw-r--r-- | 264 | unzip.hlp |
|
- | rw-r--r-- | 340 | use_file.hlp |
|
- | rw-r--r-- | 2,555 | use_file_raise_failure.hlp |
|
- | rw-r--r-- | 418 | variables.hlp |
|
- | rw-r--r-- | 1,258 | variant.hlp |
|
- | rw-r--r-- | 690 | variants.hlp |
|
- | rw-r--r-- | 1,495 | verbose.hlp |
|
- | rw-r--r-- | 1,415 | vfree_in.hlp |
|
- | rw-r--r-- | 1,204 | vsubst.hlp |
|
- | rw-r--r-- | 472 | warn.hlp |
|
- | rw-r--r-- | 278 | zip.hlp |