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