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