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