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-- | 775 | .singlefun.doc |
|
- | rw-r--r-- | 409 | .upto.doc |
|
- | rw-r--r-- | 962 | .valmod.doc |
|
- | rw-r--r-- | 1,059 | ABBREV_TAC.doc |
|
- | rw-r--r-- | 542 | ABS.doc |
|
- | rw-r--r-- | 1,037 | ABS_CONV.doc |
|
- | rw-r--r-- | 688 | ABS_TAC.doc |
|
- | rw-r--r-- | 1,967 | AC.doc |
|
- | rw-r--r-- | 909 | ACCEPT_TAC.doc |
|
- | rw-r--r-- | 769 | ADD_ASSUM.doc |
|
- | rw-r--r-- | 392 | ALL_CONV.doc |
|
- | rw-r--r-- | 1,128 | 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,344 | ASM_ARITH_TAC.doc |
|
- | rw-r--r-- | 1,055 | ASM_CASES_TAC.doc |
|
- | rw-r--r-- | 906 | 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-- | 736 | ASM_SIMP_TAC.doc |
|
- | rw-r--r-- | 1,100 | 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-- | 696 | AUGMENT_SIMPSET.doc |
|
- | rw-r--r-- | 1,101 | 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-- | 834 | BETA_TAC.doc |
|
- | rw-r--r-- | 851 | BINDER_CONV.doc |
|
- | rw-r--r-- | 923 | BINOP2_CONV.doc |
|
- | rw-r--r-- | 750 | BINOP_CONV.doc |
|
- | rw-r--r-- | 1,184 | BINOP_TAC.doc |
|
- | rw-r--r-- | 910 | BITS_ELIM_CONV.doc |
|
- | rw-r--r-- | 1,452 | BOOL_CASES_TAC.doc |
|
- | rw-r--r-- | 225 | C.doc |
|
- | rw-r--r-- | 1,149 | CACHE_CONV.doc |
|
- | rw-r--r-- | 1,417 | CASE_REWRITE_TAC.doc |
|
- | rw-r--r-- | 676 | CCONTR.doc |
|
- | rw-r--r-- | 1,287 | CHANGED_CONV.doc |
|
- | rw-r--r-- | 617 | CHANGED_TAC.doc |
|
- | rw-r--r-- | 1,139 | CHAR_EQ_CONV.doc |
|
- | rw-r--r-- | 559 | CHEAT_TAC.doc |
|
- | rw-r--r-- | 1,152 | CHOOSE_TAC.doc |
|
- | rw-r--r-- | 1,525 | CHOOSE_THEN.doc |
|
- | rw-r--r-- | 997 | CHOOSE_UPPERCASE.doc |
|
- | rw-r--r-- | 1,380 | CLAIM_TAC.doc |
|
- | rw-r--r-- | 963 | CNF_CONV.doc |
|
- | rw-r--r-- | 808 | COMB2_CONV.doc |
|
- | rw-r--r-- | 624 | COMB_CONV.doc |
|
- | rw-r--r-- | 1,576 | 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-- | 679 | CONJUNCTS_UPPERCASE.doc |
|
- | rw-r--r-- | 961 | 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,281 | 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,185 | 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-- | 410 | 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-- | 677 | 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-- | 994 | 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-- | 781 | EXPAND_TAC.doc |
|
- | rw-r--r-- | 1,008 | FAIL_TAC.doc |
|
- | rw-r--r-- | 1,727 | FIND_ASSUM.doc |
|
- | rw-r--r-- | 696 | FIRST.doc |
|
- | rw-r--r-- | 1,255 | 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,057 | FORALL_UNWIND_CONV.doc |
|
- | rw-r--r-- | 1,210 | FREEZE_THEN.doc |
|
- | rw-r--r-- | 276 | F_F.doc |
|
- | rw-r--r-- | 1,035 | GABS_CONV.doc |
|
- | rw-r--r-- | 1,012 | GEN.doc |
|
- | rw-r--r-- | 729 | 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,784 | GEN_NNF_CONV.doc |
|
- | rw-r--r-- | 1,519 | GEN_PART_MATCH.doc |
|
- | rw-r--r-- | 2,222 | 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-- | 682 | HAS_SIZE_CONV.doc |
|
- | rw-r--r-- | 794 | HAS_SIZE_DIMINDEX_RULE.doc |
|
- | rw-r--r-- | 2,175 | 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,067 | IMP_REWR_CONV.doc |
|
- | rw-r--r-- | 876 | IMP_TRANS.doc |
|
- | rw-r--r-- | 1,870 | INDUCT_TAC.doc |
|
- | rw-r--r-- | 886 | INSTANTIATE_ALL.doc |
|
- | rw-r--r-- | 1,101 | INSTANTIATE_UPPERCASE.doc |
|
- | rw-r--r-- | 1,261 | INST_TYPE.doc |
|
- | rw-r--r-- | 1,616 | INST_UPPERCASE.doc |
|
- | rw-r--r-- | 1,989 | INTEGER_RULE.doc |
|
- | rw-r--r-- | 1,237 | INTEGER_TAC.doc |
|
- | rw-r--r-- | 2,184 | 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,940 | 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-- | 803 | INT_REM_DOWN_CONV.doc |
|
- | rw-r--r-- | 2,900 | INT_RING.doc |
|
- | rw-r--r-- | 704 | INT_SGN_CONV.doc |
|
- | rw-r--r-- | 724 | INT_SUB_CONV.doc |
|
- | rw-r--r-- | 926 | ISPEC.doc |
|
- | rw-r--r-- | 962 | 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-- | 562 | 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-- | 647 | 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-- | 957 | MATCH_ACCEPT_TAC.doc |
|
- | rw-r--r-- | 2,502 | 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-- | 945 | META_EXISTS_TAC.doc |
|
- | rw-r--r-- | 970 | 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-- | 641 | 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-- | 918 | MK_EXISTS_UPPERCASE.doc |
|
- | rw-r--r-- | 914 | MK_FORALL_UPPERCASE.doc |
|
- | rw-r--r-- | 782 | MOD_DOWN_CONV.doc |
|
- | rw-r--r-- | 881 | MONO_TAC.doc |
|
- | rw-r--r-- | 763 | MP.doc |
|
- | rw-r--r-- | 1,141 | 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,381 | 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,128 | NO_TAC.doc |
|
- | rw-r--r-- | 483 | NO_THEN.doc |
|
- | rw-r--r-- | 1,137 | NUMBER_RULE.doc |
|
- | rw-r--r-- | 1,372 | 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-- | 934 | NUM_EVEN_CONV.doc |
|
- | rw-r--r-- | 1,142 | NUM_EXP_CONV.doc |
|
- | rw-r--r-- | 1,032 | NUM_FACT_CONV.doc |
|
- | rw-r--r-- | 1,072 | NUM_GE_CONV.doc |
|
- | rw-r--r-- | 1,036 | NUM_GT_CONV.doc |
|
- | rw-r--r-- | 1,078 | NUM_LE_CONV.doc |
|
- | rw-r--r-- | 1,034 | 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,200 | NUM_NORMALIZE_CONV.doc |
|
- | rw-r--r-- | 920 | NUM_ODD_CONV.doc |
|
- | rw-r--r-- | 1,031 | NUM_PRE_CONV.doc |
|
- | rw-r--r-- | 1,559 | NUM_REDUCE_CONV.doc |
|
- | rw-r--r-- | 1,300 | NUM_REDUCE_TAC.doc |
|
- | rw-r--r-- | 1,873 | NUM_RED_CONV.doc |
|
- | rw-r--r-- | 1,295 | NUM_REL_CONV.doc |
|
- | rw-r--r-- | 1,925 | NUM_RING.doc |
|
- | rw-r--r-- | 1,408 | NUM_SIMPLIFY_CONV.doc |
|
- | rw-r--r-- | 1,275 | NUM_SUB_CONV.doc |
|
- | rw-r--r-- | 985 | NUM_SUC_CONV.doc |
|
- | rw-r--r-- | 903 | NUM_TO_INT_CONV.doc |
|
- | rw-r--r-- | 1,028 | ONCE_ASM_REWRITE_RULE.doc |
|
- | rw-r--r-- | 1,806 | 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-- | 600 | ONCE_DEPTH_SQCONV.doc |
|
- | rw-r--r-- | 797 | ONCE_REWRITE_CONV.doc |
|
- | rw-r--r-- | 855 | ONCE_REWRITE_RULE.doc |
|
- | rw-r--r-- | 1,830 | ONCE_REWRITE_TAC.doc |
|
- | rw-r--r-- | 903 | ONCE_SIMPLIFY_CONV.doc |
|
- | rw-r--r-- | 776 | ONCE_SIMP_CONV.doc |
|
- | rw-r--r-- | 774 | ONCE_SIMP_RULE.doc |
|
- | rw-r--r-- | 963 | ONCE_SIMP_TAC.doc |
|
- | rw-r--r-- | 1,287 | ORDERED_IMP_REWR_CONV.doc |
|
- | rw-r--r-- | 1,816 | ORDERED_REWR_CONV.doc |
|
- | rw-r--r-- | 1,194 | 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,322 | PINST.doc |
|
- | rw-r--r-- | 2,421 | POP_ASSUM.doc |
|
- | rw-r--r-- | 1,301 | POP_ASSUM_LIST.doc |
|
- | rw-r--r-- | 758 | PRENEX_CONV.doc |
|
- | rw-r--r-- | 931 | PRESIMP_CONV.doc |
|
- | rw-r--r-- | 1,351 | 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-- | 708 | PURE_SIMP_CONV.doc |
|
- | rw-r--r-- | 744 | PURE_SIMP_RULE.doc |
|
- | rw-r--r-- | 826 | 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,481 | REAL_FIELD.doc |
|
- | rw-r--r-- | 993 | 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-- | 797 | REAL_INT_RAT_CONV.doc |
|
- | rw-r--r-- | 1,288 | REAL_INT_REDUCE_CONV.doc |
|
- | rw-r--r-- | 1,390 | 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,294 | 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,227 | REAL_POLY_MUL_CONV.doc |
|
- | rw-r--r-- | 1,169 | REAL_POLY_NEG_CONV.doc |
|
- | rw-r--r-- | 1,238 | REAL_POLY_POW_CONV.doc |
|
- | rw-r--r-- | 1,232 | 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-- | 852 | RECALL_ACCEPT_TAC.doc |
|
- | rw-r--r-- | 1,796 | REDEPTH_CONV.doc |
|
- | rw-r--r-- | 567 | REDEPTH_SQCONV.doc |
|
- | rw-r--r-- | 452 | REFL.doc |
|
- | rw-r--r-- | 477 | REFL_TAC.doc |
|
- | rw-r--r-- | 1,283 | REFUTE_THEN.doc |
|
- | rw-r--r-- | 671 | REMOVE_THEN.doc |
|
- | rw-r--r-- | 964 | REPEATC.doc |
|
- | rw-r--r-- | 839 | REPEAT_GTCL.doc |
|
- | rw-r--r-- | 1,314 | REPEAT_TCL.doc |
|
- | rw-r--r-- | 1,120 | REPEAT_UPPERCASE.doc |
|
- | rw-r--r-- | 603 | REPLICATE_TAC.doc |
|
- | rw-r--r-- | 973 | 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-- | 712 | RIGHT_BETAS.doc |
|
- | rw-r--r-- | 4,085 | RING.doc |
|
- | rw-r--r-- | 823 | 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,295 | 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-- | 845 | SET_TAC.doc |
|
- | rw-r--r-- | 878 | SIMPLE_CHOOSE.doc |
|
- | rw-r--r-- | 1,184 | SIMPLE_DISJ_CASES.doc |
|
- | rw-r--r-- | 774 | SIMPLE_EXISTS.doc |
|
- | rw-r--r-- | 882 | SIMPLIFY_CONV.doc |
|
- | rw-r--r-- | 2,163 | 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-- | 839 | STRING_EQ_CONV.doc |
|
- | rw-r--r-- | 2,345 | STRIP_ASSUME_TAC.doc |
|
- | rw-r--r-- | 2,005 | 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,915 | 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-- | 1,055 | SUBLET_CONV.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,073 | SUBST_VAR_TAC.doc |
|
- | rw-r--r-- | 1,207 | SUBS_CONV.doc |
|
- | rw-r--r-- | 1,553 | SUB_CONV.doc |
|
- | rw-r--r-- | 737 | SYM.doc |
|
- | rw-r--r-- | 452 | SYM_CONV.doc |
|
- | rw-r--r-- | 620 | TAC_PROOF.doc |
|
- | rw-r--r-- | 4,848 | TARGET_REWRITE_TAC.doc |
|
- | rw-r--r-- | 1,464 | TAUT.doc |
|
- | rw-r--r-- | 1,798 | 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,015 | TOP_SWEEP_CONV.doc |
|
- | rw-r--r-- | 647 | TOP_SWEEP_SQCONV.doc |
|
- | rw-r--r-- | 1,295 | TRANS.doc |
|
- | rw-r--r-- | 1,606 | TRANS_TAC.doc |
|
- | rw-r--r-- | 1,077 | TRY.doc |
|
- | rw-r--r-- | 530 | TRY_CONV.doc |
|
- | rw-r--r-- | 476 | UNDISCH.doc |
|
- | rw-r--r-- | 646 | UNDISCH_ALL.doc |
|
- | rw-r--r-- | 491 | UNDISCH_TAC.doc |
|
- | rw-r--r-- | 668 | UNDISCH_THEN.doc |
|
- | rw-r--r-- | 2,043 | UNIFY_ACCEPT_TAC.doc |
|
- | rw-r--r-- | 948 | UNWIND_CONV.doc |
|
- | rw-r--r-- | 559 | USE_THEN.doc |
|
- | rw-r--r-- | 1,282 | VALID.doc |
|
- | rw-r--r-- | 203 | W.doc |
|
- | rw-r--r-- | 1,102 | 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,115 | X_CHOOSE_THEN.doc |
|
- | rw-r--r-- | 911 | X_GEN_TAC.doc |
|
- | rw-r--r-- | 971 | 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-- | 674 | alpha.doc |
|
- | rw-r--r-- | 1,075 | alphaorder.doc |
|
- | rw-r--r-- | 753 | 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-- | 655 | assocd.doc |
|
- | rw-r--r-- | 1,035 | atleast.doc |
|
- | rw-r--r-- | 408 | aty.doc |
|
- | rw-r--r-- | 1,263 | augment.doc |
|
- | rw-r--r-- | 725 | axioms.doc |
|
- | rw-r--r-- | 1,015 | b.doc |
|
- | rw-r--r-- | 1,389 | basic_congs.doc |
|
- | rw-r--r-- | 1,172 | basic_convs.doc |
|
- | rw-r--r-- | 679 | basic_net.doc |
|
- | rw-r--r-- | 846 | basic_prover.doc |
|
- | rw-r--r-- | 721 | basic_rectype_net.doc |
|
- | rw-r--r-- | 1,826 | basic_rewrites.doc |
|
- | rw-r--r-- | 586 | basic_ss.doc |
|
- | rw-r--r-- | 580 | binders.doc |
|
- | rw-r--r-- | 736 | binops.doc |
|
- | rw-r--r-- | 294 | bndvar.doc |
|
- | rw-r--r-- | 280 | body.doc |
|
- | rw-r--r-- | 347 | bool_ty.doc |
|
- | rw-r--r-- | 408 | bty.doc |
|
- | rw-r--r-- | 269 | butlast.doc |
|
- | rw-r--r-- | 320 | by.doc |
|
- | rw-r--r-- | 387 | can.doc |
|
- | rw-r--r-- | 809 | cases.doc |
|
- | rw-r--r-- | 609 | check.doc |
|
- | rw-r--r-- | 855 | checkpoint.doc |
|
- | rw-r--r-- | 1,015 | choose.doc |
|
- | rw-r--r-- | 430 | chop_list.doc |
|
- | rw-r--r-- | 1,838 | combine.doc |
|
- | rw-r--r-- | 1,304 | comment_token.doc |
|
- | rw-r--r-- | 737 | compose_insts.doc |
|
- | rw-r--r-- | 410 | concl.doc |
|
- | rw-r--r-- | 1,167 | conjuncts.doc |
|
- | rw-r--r-- | 307 | constants.doc |
|
- | rw-r--r-- | 378 | copverb.doc |
|
- | rw-r--r-- | 460 | current_goalstack.doc |
|
- | rw-r--r-- | 453 | curry.doc |
|
- | rw-r--r-- | 592 | decreasing.doc |
|
- | rw-r--r-- | 973 | deep_alpha.doc |
|
- | rw-r--r-- | 3,265 | define.doc |
|
- | rw-r--r-- | 2,741 | define_quotient_type.doc |
|
- | rw-r--r-- | 6,117 | define_type.doc |
|
- | rw-r--r-- | 701 | define_type_raw.doc |
|
- | rw-r--r-- | 845 | defined.doc |
|
- | rw-r--r-- | 955 | definitions.doc |
|
- | rw-r--r-- | 480 | delete_parser.doc |
|
- | rw-r--r-- | 732 | delete_user_printer.doc |
|
- | rw-r--r-- | 621 | denominator.doc |
|
- | rw-r--r-- | 2,394 | derive_nonschematic_inductive_relations.doc |
|
- | rw-r--r-- | 2,583 | derive_strong_induction.doc |
|
- | rw-r--r-- | 456 | dest_abs.doc |
|
- | rw-r--r-- | 596 | dest_binary.doc |
|
- | rw-r--r-- | 658 | dest_binder.doc |
|
- | rw-r--r-- | 619 | dest_binop.doc |
|
- | rw-r--r-- | 669 | dest_char.doc |
|
- | rw-r--r-- | 671 | 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-- | 559 | dest_finty.doc |
|
- | rw-r--r-- | 405 | dest_forall.doc |
|
- | rw-r--r-- | 622 | dest_fun_ty.doc |
|
- | rw-r--r-- | 930 | dest_gabs.doc |
|
- | rw-r--r-- | 594 | 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-- | 867 | dest_numeral.doc |
|
- | rw-r--r-- | 412 | dest_pair.doc |
|
- | rw-r--r-- | 652 | dest_realintconst.doc |
|
- | rw-r--r-- | 365 | dest_select.doc |
|
- | rw-r--r-- | 715 | 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-- | 386 | dest_uexists.doc |
|
- | rw-r--r-- | 389 | dest_var.doc |
|
- | rw-r--r-- | 472 | dest_vartype.doc |
|
- | rw-r--r-- | 1,157 | disjuncts.doc |
|
- | rw-r--r-- | 911 | distinctness.doc |
|
- | rw-r--r-- | 446 | distinctness_store.doc |
|
- | rw-r--r-- | 674 | do_list.doc |
|
- | rw-r--r-- | 843 | dom.doc |
|
- | rw-r--r-- | 238 | 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-- | 502 | empty_ss.doc |
|
- | rw-r--r-- | 447 | end_itlist.doc |
|
- | rw-r--r-- | 2,269 | enter.doc |
|
- | rw-r--r-- | 556 | equals_goal.doc |
|
- | rw-r--r-- | 517 | equals_thm.doc |
|
- | rw-r--r-- | 253 | exactly.doc |
|
- | rw-r--r-- | 567 | exists.doc |
|
- | rw-r--r-- | 462 | explode.doc |
|
- | rw-r--r-- | 1,281 | extend_basic_congs.doc |
|
- | rw-r--r-- | 1,335 | 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-- | 652 | 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-- | 811 | find_path.doc |
|
- | rw-r--r-- | 449 | find_term.doc |
|
- | rw-r--r-- | 598 | 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-- | 497 | flush_goalstack.doc |
|
- | rw-r--r-- | 1,377 | foldl.doc |
|
- | rw-r--r-- | 1,424 | foldr.doc |
|
- | rw-r--r-- | 760 | follow_path.doc |
|
- | rw-r--r-- | 560 | forall.doc |
|
- | rw-r--r-- | 724 | forall2.doc |
|
- | rw-r--r-- | 897 | free_in.doc |
|
- | rw-r--r-- | 553 | frees.doc |
|
- | rw-r--r-- | 739 | freesin.doc |
|
- | rw-r--r-- | 635 | freesl.doc |
|
- | rw-r--r-- | 736 | funpow.doc |
|
- | rw-r--r-- | 603 | g.doc |
|
- | rw-r--r-- | 529 | gcd.doc |
|
- | rw-r--r-- | 669 | 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-- | 607 | get_type_arity.doc |
|
- | rw-r--r-- | 902 | graph.doc |
|
- | rw-r--r-- | 213 | hd.doc |
|
- | rw-r--r-- | 1,722 | help.doc |
|
- | rw-r--r-- | 607 | help_path.doc |
|
- | rw-r--r-- | 644 | hide_constant.doc |
|
- | rw-r--r-- | 688 | hol_dir.doc |
|
- | rw-r--r-- | 766 | 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-- | 946 | ignore_constant_varstruct.doc |
|
- | rw-r--r-- | 544 | implode.doc |
|
- | rw-r--r-- | 656 | increasing.doc |
|
- | rw-r--r-- | 557 | index.doc |
|
- | rw-r--r-- | 1,632 | inductive_type_store.doc |
|
- | rw-r--r-- | 447 | infixes.doc |
|
- | rw-r--r-- | 961 | injectivity.doc |
|
- | rw-r--r-- | 448 | injectivity_store.doc |
|
- | rw-r--r-- | 547 | insert.doc |
|
- | rw-r--r-- | 768 | insert_prime.doc |
|
- | rw-r--r-- | 1,361 | inst.doc |
|
- | rw-r--r-- | 572 | inst_goal.doc |
|
- | rw-r--r-- | 547 | install_parser.doc |
|
- | rw-r--r-- | 2,034 | install_user_printer.doc |
|
- | rw-r--r-- | 489 | 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-- | 655 | intersect.doc |
|
- | rw-r--r-- | 402 | is_abs.doc |
|
- | rw-r--r-- | 703 | is_binary.doc |
|
- | rw-r--r-- | 705 | 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-- | 595 | 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-- | 287 | 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-- | 321 | is_numeral.doc |
|
- | rw-r--r-- | 368 | is_pair.doc |
|
- | rw-r--r-- | 421 | is_prefix.doc |
|
- | rw-r--r-- | 720 | is_ratconst.doc |
|
- | rw-r--r-- | 596 | is_realintconst.doc |
|
- | rw-r--r-- | 456 | is_reserved_word.doc |
|
- | rw-r--r-- | 280 | is_select.doc |
|
- | rw-r--r-- | 544 | is_setenum.doc |
|
- | rw-r--r-- | 492 | is_type.doc |
|
- | rw-r--r-- | 341 | is_uexists.doc |
|
- | rw-r--r-- | 838 | is_undefined.doc |
|
- | rw-r--r-- | 380 | is_var.doc |
|
- | rw-r--r-- | 466 | is_vartype.doc |
|
- | rw-r--r-- | 430 | isalnum.doc |
|
- | rw-r--r-- | 417 | isalpha.doc |
|
- | rw-r--r-- | 421 | isbra.doc |
|
- | rw-r--r-- | 348 | isnum.doc |
|
- | rw-r--r-- | 365 | issep.doc |
|
- | rw-r--r-- | 389 | isspace.doc |
|
- | rw-r--r-- | 695 | issymb.doc |
|
- | rw-r--r-- | 492 | it.doc |
|
- | rw-r--r-- | 490 | itlist.doc |
|
- | rw-r--r-- | 674 | itlist2.doc |
|
- | rw-r--r-- | 222 | last.doc |
|
- | rw-r--r-- | 551 | lcm_num.doc |
|
- | rw-r--r-- | 1,545 | leftbin.doc |
|
- | rw-r--r-- | 170 | length.doc |
|
- | rw-r--r-- | 2,001 | let_CONV.doc |
|
- | rw-r--r-- | 1,537 | lex.doc |
|
- | rw-r--r-- | 953 | lhand.doc |
|
- | rw-r--r-- | 301 | lhs.doc |
|
- | rw-r--r-- | 4,542 | lift_function.doc |
|
- | rw-r--r-- | 3,472 | lift_theorem.doc |
|
- | rw-r--r-- | 413 | list_mk_abs.doc |
|
- | rw-r--r-- | 1,040 | 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-- | 523 | list_mk_gabs.doc |
|
- | rw-r--r-- | 977 | 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-- | 527 | loaded_files.doc |
|
- | rw-r--r-- | 761 | loads.doc |
|
- | rw-r--r-- | 904 | loadt.doc |
|
- | rw-r--r-- | 2,685 | lookup.doc |
|
- | rw-r--r-- | 621 | 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-- | 417 | map2.doc |
|
- | rw-r--r-- | 940 | mapf.doc |
|
- | rw-r--r-- | 682 | mapfilter.doc |
|
- | rw-r--r-- | 314 | mem.doc |
|
- | rw-r--r-- | 810 | mem_prime.doc |
|
- | rw-r--r-- | 649 | merge.doc |
|
- | rw-r--r-- | 1,116 | merge_nets.doc |
|
- | rw-r--r-- | 727 | mergesort.doc |
|
- | rw-r--r-- | 1,014 | meson_brand.doc |
|
- | rw-r--r-- | 714 | meson_chatty.doc |
|
- | rw-r--r-- | 768 | meson_dcutin.doc |
|
- | rw-r--r-- | 811 | meson_depth.doc |
|
- | rw-r--r-- | 912 | meson_prefine.doc |
|
- | rw-r--r-- | 992 | meson_skew.doc |
|
- | rw-r--r-- | 954 | meson_split_limit.doc |
|
- | rw-r--r-- | 353 | metisverb.doc |
|
- | rw-r--r-- | 475 | mk_abs.doc |
|
- | rw-r--r-- | 824 | mk_binary.doc |
|
- | rw-r--r-- | 737 | mk_binder.doc |
|
- | rw-r--r-- | 655 | mk_binop.doc |
|
- | rw-r--r-- | 578 | 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-- | 970 | 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-- | 616 | mk_flist.doc |
|
- | rw-r--r-- | 406 | mk_forall.doc |
|
- | rw-r--r-- | 818 | mk_fset.doc |
|
- | rw-r--r-- | 787 | mk_fthm.doc |
|
- | rw-r--r-- | 500 | mk_fun_ty.doc |
|
- | rw-r--r-- | 1,346 | mk_gabs.doc |
|
- | rw-r--r-- | 400 | mk_goalstate.doc |
|
- | rw-r--r-- | 769 | mk_icomb.doc |
|
- | rw-r--r-- | 522 | mk_iff.doc |
|
- | rw-r--r-- | 351 | mk_imp.doc |
|
- | rw-r--r-- | 727 | mk_intconst.doc |
|
- | rw-r--r-- | 681 | mk_let.doc |
|
- | rw-r--r-- | 711 | mk_list.doc |
|
- | rw-r--r-- | 939 | mk_mconst.doc |
|
- | rw-r--r-- | 332 | mk_neg.doc |
|
- | rw-r--r-- | 771 | mk_numeral.doc |
|
- | rw-r--r-- | 304 | mk_pair.doc |
|
- | rw-r--r-- | 958 | mk_primed_var.doc |
|
- | rw-r--r-- | 1,794 | mk_prover.doc |
|
- | rw-r--r-- | 755 | mk_realintconst.doc |
|
- | rw-r--r-- | 1,237 | mk_rewrites.doc |
|
- | rw-r--r-- | 254 | mk_select.doc |
|
- | rw-r--r-- | 840 | mk_setenum.doc |
|
- | rw-r--r-- | 694 | mk_small_numeral.doc |
|
- | rw-r--r-- | 480 | 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-- | 786 | 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-- | 590 | new_constant.doc |
|
- | rw-r--r-- | 1,652 | new_definition.doc |
|
- | rw-r--r-- | 5,056 | new_inductive_definition.doc |
|
- | rw-r--r-- | 3,462 | 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-- | 583 | nsplit.doc |
|
- | rw-r--r-- | 537 | null_inst.doc |
|
- | rw-r--r-- | 485 | null_meta.doc |
|
- | rw-r--r-- | 377 | 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-- | 672 | numdom.doc |
|
- | rw-r--r-- | 609 | numerator.doc |
|
- | rw-r--r-- | 199 | o.doc |
|
- | rw-r--r-- | 628 | 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,174 | parse_as_infix.doc |
|
- | rw-r--r-- | 472 | parse_as_prefix.doc |
|
- | rw-r--r-- | 756 | parse_inductive_type_specification.doc |
|
- | rw-r--r-- | 602 | parse_preterm.doc |
|
- | rw-r--r-- | 602 | parse_pretype.doc |
|
- | rw-r--r-- | 765 | parse_term.doc |
|
- | rw-r--r-- | 475 | parse_type.doc |
|
- | rw-r--r-- | 548 | parses_as_binder.doc |
|
- | rw-r--r-- | 499 | 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-- | 480 | pp_print_qterm.doc |
|
- | rw-r--r-- | 503 | pp_print_qtype.doc |
|
- | rw-r--r-- | 487 | pp_print_term.doc |
|
- | rw-r--r-- | 405 | pp_print_thm.doc |
|
- | rw-r--r-- | 501 | pp_print_type.doc |
|
- | rw-r--r-- | 883 | prebroken_binops.doc |
|
- | rw-r--r-- | 604 | prefixes.doc |
|
- | rw-r--r-- | 583 | preterm_of_term.doc |
|
- | rw-r--r-- | 587 | 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-- | 418 | 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-- | 350 | print_thm.doc |
|
- | rw-r--r-- | 777 | 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-- | 723 | prove_monotonicity_hyps.doc |
|
- | rw-r--r-- | 3,540 | 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-- | 571 | quotexpander.doc |
|
- | rw-r--r-- | 1,008 | r.doc |
|
- | rw-r--r-- | 811 | ran.doc |
|
- | rw-r--r-- | 353 | rand.doc |
|
- | rw-r--r-- | 739 | rat_of_term.doc |
|
- | rw-r--r-- | 447 | rator.doc |
|
- | rw-r--r-- | 1,910 | real_ideal_cofactors.doc |
|
- | rw-r--r-- | 586 | reduce_interface.doc |
|
- | rw-r--r-- | 558 | refine.doc |
|
- | rw-r--r-- | 665 | remark.doc |
|
- | rw-r--r-- | 418 | remove.doc |
|
- | rw-r--r-- | 573 | remove_interface.doc |
|
- | rw-r--r-- | 818 | remove_type_abbrev.doc |
|
- | rw-r--r-- | 562 | repeat.doc |
|
- | rw-r--r-- | 283 | replicate.doc |
|
- | rw-r--r-- | 345 | report.doc |
|
- | rw-r--r-- | 806 | report_timing.doc |
|
- | rw-r--r-- | 537 | reserve_words.doc |
|
- | rw-r--r-- | 637 | reserved_words.doc |
|
- | rw-r--r-- | 737 | retypecheck.doc |
|
- | rw-r--r-- | 172 | rev.doc |
|
- | rw-r--r-- | 521 | 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,335 | reverse_interface_mapping.doc |
|
- | rw-r--r-- | 287 | rhs.doc |
|
- | rw-r--r-- | 1,553 | rightbin.doc |
|
- | rw-r--r-- | 359 | rotate.doc |
|
- | rw-r--r-- | 2,540 | search.doc |
|
- | rw-r--r-- | 2,351 | self_destruct.doc |
|
- | rw-r--r-- | 725 | set_basic_congs.doc |
|
- | rw-r--r-- | 942 | set_basic_convs.doc |
|
- | rw-r--r-- | 740 | set_basic_rewrites.doc |
|
- | rw-r--r-- | 542 | set_eq.doc |
|
- | rw-r--r-- | 1,976 | set_goal.doc |
|
- | rw-r--r-- | 490 | setify.doc |
|
- | rw-r--r-- | 702 | shareout.doc |
|
- | rw-r--r-- | 964 | some.doc |
|
- | rw-r--r-- | 1,900 | sort.doc |
|
- | rw-r--r-- | 700 | splitlist.doc |
|
- | rw-r--r-- | 834 | ss_of_congs.doc |
|
- | rw-r--r-- | 858 | ss_of_conv.doc |
|
- | rw-r--r-- | 930 | ss_of_maker.doc |
|
- | rw-r--r-- | 895 | ss_of_prover.doc |
|
- | rw-r--r-- | 795 | ss_of_provers.doc |
|
- | rw-r--r-- | 847 | ss_of_thms.doc |
|
- | rw-r--r-- | 694 | startup_banner.doc |
|
- | rw-r--r-- | 655 | string_of_file.doc |
|
- | rw-r--r-- | 604 | string_of_term.doc |
|
- | rw-r--r-- | 834 | string_of_thm.doc |
|
- | rw-r--r-- | 478 | string_of_type.doc |
|
- | rw-r--r-- | 705 | 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-- | 709 | strip_gabs.doc |
|
- | rw-r--r-- | 878 | strip_ncomb.doc |
|
- | rw-r--r-- | 670 | striplist.doc |
|
- | rw-r--r-- | 513 | 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-- | 388 | temp_path.doc |
|
- | rw-r--r-- | 1,237 | term_match.doc |
|
- | rw-r--r-- | 702 | term_of_preterm.doc |
|
- | rw-r--r-- | 687 | term_of_rat.doc |
|
- | rw-r--r-- | 1,079 | term_order.doc |
|
- | rw-r--r-- | 768 | term_type_unify.doc |
|
- | rw-r--r-- | 814 | term_unify.doc |
|
- | rw-r--r-- | 838 | term_union.doc |
|
- | rw-r--r-- | 1,913 | the_definitions.doc |
|
- | rw-r--r-- | 1,784 | the_implicit_types.doc |
|
- | rw-r--r-- | 1,286 | the_inductive_definitions.doc |
|
- | rw-r--r-- | 423 | the_inductive_types.doc |
|
- | rw-r--r-- | 552 | the_interface.doc |
|
- | rw-r--r-- | 1,533 | the_overload_skeletons.doc |
|
- | rw-r--r-- | 1,027 | the_specifications.doc |
|
- | rw-r--r-- | 1,239 | 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-- | 511 | top_realgoal.doc |
|
- | rw-r--r-- | 790 | top_thm.doc |
|
- | rw-r--r-- | 533 | try_user_parser.doc |
|
- | rw-r--r-- | 975 | try_user_printer.doc |
|
- | rw-r--r-- | 904 | tryapplyd.doc |
|
- | rw-r--r-- | 523 | tryfind.doc |
|
- | rw-r--r-- | 361 | type_abbrevs.doc |
|
- | rw-r--r-- | 1,456 | type_invention_error.doc |
|
- | rw-r--r-- | 1,744 | type_invention_warning.doc |
|
- | rw-r--r-- | 1,349 | type_match.doc |
|
- | rw-r--r-- | 181 | type_of.doc |
|
- | rw-r--r-- | 637 | type_of_pretype.doc |
|
- | rw-r--r-- | 739 | type_subst.doc |
|
- | rw-r--r-- | 590 | type_unify.doc |
|
- | rw-r--r-- | 639 | type_vars_in_term.doc |
|
- | rw-r--r-- | 713 | types.doc |
|
- | rw-r--r-- | 1,170 | 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-- | 944 | undefine.doc |
|
- | rw-r--r-- | 803 | undefined.doc |
|
- | rw-r--r-- | 654 | unhide_constant.doc |
|
- | rw-r--r-- | 570 | union.doc |
|
- | rw-r--r-- | 834 | union_prime.doc |
|
- | rw-r--r-- | 457 | unions.doc |
|
- | rw-r--r-- | 683 | unions_prime.doc |
|
- | rw-r--r-- | 445 | uniq.doc |
|
- | rw-r--r-- | 833 | unparse_as_binder.doc |
|
- | rw-r--r-- | 618 | unparse_as_infix.doc |
|
- | rw-r--r-- | 502 | unparse_as_prefix.doc |
|
- | rw-r--r-- | 714 | unreserve_words.doc |
|
- | rw-r--r-- | 920 | unspaced_binops.doc |
|
- | rw-r--r-- | 264 | unzip.doc |
|
- | rw-r--r-- | 340 | use_file.doc |
|
- | rw-r--r-- | 418 | variables.doc |
|
- | rw-r--r-- | 1,258 | variant.doc |
|
- | rw-r--r-- | 690 | variants.doc |
|
- | rw-r--r-- | 1,495 | verbose.doc |
|
- | rw-r--r-- | 1,415 | vfree_in.doc |
|
- | rw-r--r-- | 1,204 | vsubst.doc |
|
- | rw-r--r-- | 472 | warn.doc |
|
- | rw-r--r-- | 278 | zip.doc |