package info
(click to toggle)
hol88 2.02.19940316dfsg-5
- links: PTS
- area: main
- in suites: bookworm
- size: 65,816 kB
- sloc: ml: 199,939; ansic: 9,666; sh: 6,913; makefile: 6,032; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
Folder: ENTRIES
 |
.. (parent) | |||
 |
- | rw-r--r-- | 258 | %23.doc |
|
- | rw-r--r-- | 126 | %2A.doc |
|
- | rw-r--r-- | 150 | %2B.doc |
|
- | rw-r--r-- | 307 | -.doc |
|
- | rw-r--r-- | 319 | ..doc |
|
- | rw-r--r-- | 164 | .div.doc |
|
- | rw-r--r-- | 545 | .hat.doc |
|
- | rw-r--r-- | 166 | %3C.doc |
|
- | rw-r--r-- | 479 | %3C%3C.doc |
|
- | rw-r--r-- | 761 | %3D.doc |
|
- | rw-r--r-- | 169 | %3E.doc |
|
- | rw-r--r-- | 297 | %40.doc |
|
- | rw-r--r-- | 467 | ABS.doc |
|
- | rw-r--r-- | 912 | ABS_CONV.doc |
|
- | rw-r--r-- | 805 | ACCEPT_TAC.doc |
|
- | rw-r--r-- | 1,223 | AC_CONV.doc |
|
- | rw-r--r-- | 687 | ADD_ASSUM.doc |
|
- | rw-r--r-- | 552 | ADD_CONV.doc |
|
- | rw-r--r-- | 337 | ALL_CONV.doc |
|
- | rw-r--r-- | 1,159 | ALL_EL_CONV.doc |
|
- | rw-r--r-- | 680 | ALL_TAC.doc |
|
- | rw-r--r-- | 715 | ALL_THEN.doc |
|
- | rw-r--r-- | 580 | ALPHA.doc |
|
- | rw-r--r-- | 707 | ALPHA_CONV.doc |
|
- | rw-r--r-- | 640 | AND_EXISTS_CONV.doc |
|
- | rw-r--r-- | 479 | AND_FORALL_CONV.doc |
|
- | rw-r--r-- | 651 | ANTE_CONJ_CONV.doc |
|
- | rw-r--r-- | 1,899 | ANTE_RES_THEN.doc |
|
- | rw-r--r-- | 680 | APPEND_CONV.doc |
|
- | rw-r--r-- | 539 | AP_TERM.doc |
|
- | rw-r--r-- | 505 | AP_TERM_TAC.doc |
|
- | rw-r--r-- | 637 | AP_THM.doc |
|
- | rw-r--r-- | 560 | AP_THM_TAC.doc |
|
- | rw-r--r-- | 1,124 | ASM_CASES_TAC.doc |
|
- | rw-r--r-- | 982 | ASM_REWRITE_RULE.doc |
|
- | rw-r--r-- | 1,599 | ASM_REWRITE_TAC.doc |
|
- | rw-r--r-- | 429 | ASSUME.doc |
|
- | rw-r--r-- | 2,013 | ASSUME_TAC.doc |
|
- | rw-r--r-- | 1,407 | ASSUM_LIST.doc |
|
- | rw-r--r-- | 244 | B.doc |
|
- | rw-r--r-- | 1,128 | BETA_CONV.doc |
|
- | rw-r--r-- | 914 | BETA_RULE.doc |
|
- | rw-r--r-- | 597 | BETA_TAC.doc |
|
- | rw-r--r-- | 966 | BODY_CONJUNCTS.doc |
|
- | rw-r--r-- | 1,294 | BOOL_CASES_TAC.doc |
|
- | rw-r--r-- | 576 | BUTFIRSTN_CONV.doc |
|
- | rw-r--r-- | 565 | BUTLASTN_CONV.doc |
|
- | rw-r--r-- | 454 | BUTLAST_CONV.doc |
|
- | rw-r--r-- | 251 | C.doc |
|
- | rw-r--r-- | 1,603 | CASES_THENL.doc |
|
- | rw-r--r-- | 225 | CB.doc |
|
- | rw-r--r-- | 688 | CCONTR.doc |
|
- | rw-r--r-- | 1,283 | CHANGED_CONV.doc |
|
- | rw-r--r-- | 466 | CHANGED_TAC.doc |
|
- | rw-r--r-- | 978 | CHECK_ASSUME_TAC.doc |
|
- | rw-r--r-- | 917 | CHOOSE.doc |
|
- | rw-r--r-- | 1,154 | CHOOSE_TAC.doc |
|
- | rw-r--r-- | 1,507 | CHOOSE_THEN.doc |
|
- | rw-r--r-- | 1,882 | COND_CASES_TAC.doc |
|
- | rw-r--r-- | 620 | COND_CONV.doc |
|
- | rw-r--r-- | 337 | CONJ.doc |
|
- | rw-r--r-- | 357 | CONJUNCT1.doc |
|
- | rw-r--r-- | 358 | CONJUNCT2.doc |
|
- | rw-r--r-- | 757 | CONJUNCTS.doc |
|
- | rw-r--r-- | 1,075 | CONJUNCTS_CONV.doc |
|
- | rw-r--r-- | 1,417 | CONJUNCTS_THEN.doc |
|
- | rw-r--r-- | 1,191 | CONJUNCTS_THEN2.doc |
|
- | rw-r--r-- | 704 | CONJ_DISCH.doc |
|
- | rw-r--r-- | 778 | CONJ_DISCHL.doc |
|
- | rw-r--r-- | 1,396 | CONJ_LIST.doc |
|
- | rw-r--r-- | 454 | CONJ_PAIR.doc |
|
- | rw-r--r-- | 1,019 | CONJ_SET_CONV.doc |
|
- | rw-r--r-- | 467 | CONJ_TAC.doc |
|
- | rw-r--r-- | 459 | CONTR.doc |
|
- | rw-r--r-- | 467 | CONTRAPOS.doc |
|
- | rw-r--r-- | 413 | CONTRAPOS_CONV.doc |
|
- | rw-r--r-- | 534 | CONTR_TAC.doc |
|
- | rw-r--r-- | 1,004 | CONV_RULE.doc |
|
- | rw-r--r-- | 1,870 | CONV_TAC.doc |
|
- | rw-r--r-- | 280 | Co.doc |
|
- | rw-r--r-- | 1,043 | DEF_EXISTS_RULE.doc |
|
- | rw-r--r-- | 2,815 | DEPTH_CONV.doc |
|
- | rw-r--r-- | 654 | DISCARD_TAC.doc |
|
- | rw-r--r-- | 551 | DISCH.doc |
|
- | rw-r--r-- | 781 | DISCH_ALL.doc |
|
- | rw-r--r-- | 849 | DISCH_TAC.doc |
|
- | rw-r--r-- | 1,383 | DISCH_THEN.doc |
|
- | rw-r--r-- | 463 | DISJ1.doc |
|
- | rw-r--r-- | 302 | DISJ1_TAC.doc |
|
- | rw-r--r-- | 383 | DISJ2.doc |
|
- | rw-r--r-- | 307 | DISJ2_TAC.doc |
|
- | rw-r--r-- | 1,406 | DISJ_CASES.doc |
|
- | rw-r--r-- | 975 | DISJ_CASES_TAC.doc |
|
- | rw-r--r-- | 1,598 | DISJ_CASES_THEN.doc |
|
- | rw-r--r-- | 1,903 | DISJ_CASES_THEN2.doc |
|
- | rw-r--r-- | 1,462 | DISJ_CASES_THENL.doc |
|
- | rw-r--r-- | 1,167 | DISJ_CASES_UNION.doc |
|
- | rw-r--r-- | 642 | DISJ_IMP.doc |
|
- | rw-r--r-- | 640 | ELL_CONV.doc |
|
- | rw-r--r-- | 503 | EL_CONV.doc |
|
- | rw-r--r-- | 330 | EQF_ELIM.doc |
|
- | rw-r--r-- | 317 | EQF_INTRO.doc |
|
- | rw-r--r-- | 308 | EQT_ELIM.doc |
|
- | rw-r--r-- | 260 | EQT_INTRO.doc |
|
- | rw-r--r-- | 643 | EQ_IMP_RULE.doc |
|
- | rw-r--r-- | 1,433 | EQ_LENGTH_INDUCT_TAC.doc |
|
- | rw-r--r-- | 1,467 | EQ_LENGTH_SNOC_INDUCT_TAC.doc |
|
- | rw-r--r-- | 606 | EQ_MP.doc |
|
- | rw-r--r-- | 585 | EQ_TAC.doc |
|
- | rw-r--r-- | 315 | ETA_CONV.doc |
|
- | rw-r--r-- | 831 | EVERY.doc |
|
- | rw-r--r-- | 907 | EVERY_ASSUM.doc |
|
- | rw-r--r-- | 825 | EVERY_CONV.doc |
|
- | rw-r--r-- | 803 | EVERY_TCL.doc |
|
- | rw-r--r-- | 517 | EXISTENCE.doc |
|
- | rw-r--r-- | 931 | EXISTS.doc |
|
- | rw-r--r-- | 1,012 | EXISTS_AND_CONV.doc |
|
- | rw-r--r-- | 825 | EXISTS_EQ.doc |
|
- | rw-r--r-- | 721 | EXISTS_GREATEST_CONV.doc |
|
- | rw-r--r-- | 716 | EXISTS_IMP.doc |
|
- | rw-r--r-- | 1,005 | EXISTS_IMP_CONV.doc |
|
- | rw-r--r-- | 916 | EXISTS_LEAST_CONV.doc |
|
- | rw-r--r-- | 455 | EXISTS_NOT_CONV.doc |
|
- | rw-r--r-- | 489 | EXISTS_OR_CONV.doc |
|
- | rw-r--r-- | 786 | EXISTS_TAC.doc |
|
- | rw-r--r-- | 999 | EXISTS_UNIQUE_CONV.doc |
|
- | rw-r--r-- | 576 | EXT.doc |
|
- | rw-r--r-- | 944 | FAIL_TAC.doc |
|
- | rw-r--r-- | 1,543 | FILTER_ASM_REWRITE_RULE.doc |
|
- | rw-r--r-- | 1,825 | FILTER_ASM_REWRITE_TAC.doc |
|
- | rw-r--r-- | 962 | FILTER_CONV.doc |
|
- | rw-r--r-- | 1,362 | FILTER_DISCH_TAC.doc |
|
- | rw-r--r-- | 1,326 | FILTER_DISCH_THEN.doc |
|
- | rw-r--r-- | 882 | FILTER_GEN_TAC.doc |
|
- | rw-r--r-- | 1,149 | FILTER_ONCE_ASM_REWRITE_RULE.doc |
|
- | rw-r--r-- | 1,123 | FILTER_ONCE_ASM_REWRITE_TAC.doc |
|
- | rw-r--r-- | 1,463 | FILTER_PURE_ASM_REWRITE_RULE.doc |
|
- | rw-r--r-- | 1,749 | FILTER_PURE_ASM_REWRITE_TAC.doc |
|
- | rw-r--r-- | 1,088 | FILTER_PURE_ONCE_ASM_REWRITE_RULE.doc |
|
- | rw-r--r-- | 1,062 | FILTER_PURE_ONCE_ASM_REWRITE_TAC.doc |
|
- | rw-r--r-- | 2,803 | FILTER_STRIP_TAC.doc |
|
- | rw-r--r-- | 1,632 | FILTER_STRIP_THEN.doc |
|
- | rw-r--r-- | 698 | FIRST.doc |
|
- | rw-r--r-- | 552 | FIRSTN_CONV.doc |
|
- | rw-r--r-- | 1,160 | FIRST_ASSUM.doc |
|
- | rw-r--r-- | 597 | FIRST_CONV.doc |
|
- | rw-r--r-- | 723 | FIRST_TCL.doc |
|
- | rw-r--r-- | 667 | FLAT_CONV.doc |
|
- | rw-r--r-- | 1,360 | FOLDL_CONV.doc |
|
- | rw-r--r-- | 1,360 | FOLDR_CONV.doc |
|
- | rw-r--r-- | 490 | FORALL_AND_CONV.doc |
|
- | rw-r--r-- | 778 | FORALL_EQ.doc |
|
- | rw-r--r-- | 1,000 | FORALL_IMP_CONV.doc |
|
- | rw-r--r-- | 450 | FORALL_NOT_CONV.doc |
|
- | rw-r--r-- | 1,000 | FORALL_OR_CONV.doc |
|
- | rw-r--r-- | 1,795 | FREEZE_THEN.doc |
|
- | rw-r--r-- | 827 | FRONT_CONJ_CONV.doc |
|
- | rw-r--r-- | 769 | FUN_EQ_CONV.doc |
|
- | rw-r--r-- | 941 | GEN.doc |
|
- | rw-r--r-- | 757 | GENL.doc |
|
- | rw-r--r-- | 543 | GEN_ALL.doc |
|
- | rw-r--r-- | 1,559 | GEN_ALPHA_CONV.doc |
|
- | rw-r--r-- | 1,488 | GEN_BETA_CONV.doc |
|
- | rw-r--r-- | 3,065 | GEN_REWRITE_CONV.doc |
|
- | rw-r--r-- | 3,183 | GEN_REWRITE_RULE.doc |
|
- | rw-r--r-- | 3,482 | GEN_REWRITE_TAC.doc |
|
- | rw-r--r-- | 799 | GEN_TAC.doc |
|
- | rw-r--r-- | 759 | GSPEC.doc |
|
- | rw-r--r-- | 1,855 | GSUBST_TAC.doc |
|
- | rw-r--r-- | 810 | GSYM.doc |
|
- | rw-r--r-- | 685 | HALF_MK_ABS.doc |
|
- | rw-r--r-- | 195 | I.doc |
|
- | rw-r--r-- | 635 | IMP_ANTISYM_RULE.doc |
|
- | rw-r--r-- | 1,091 | IMP_CANON.doc |
|
- | rw-r--r-- | 537 | IMP_CONJ.doc |
|
- | rw-r--r-- | 429 | IMP_ELIM.doc |
|
- | rw-r--r-- | 1,662 | IMP_RES_TAC.doc |
|
- | rw-r--r-- | 3,879 | IMP_RES_THEN.doc |
|
- | rw-r--r-- | 642 | IMP_TRANS.doc |
|
- | rw-r--r-- | 877 | INDUCT.doc |
|
- | rw-r--r-- | 1,037 | INDUCT_TAC.doc |
|
- | rw-r--r-- | 4,100 | INDUCT_THEN.doc |
|
- | rw-r--r-- | 825 | INST.doc |
|
- | rw-r--r-- | 1,340 | INST_TYPE.doc |
|
- | rw-r--r-- | 548 | INST_TY_TERM.doc |
|
- | rw-r--r-- | 722 | ISPEC.doc |
|
- | rw-r--r-- | 674 | ISPECL.doc |
|
- | rw-r--r-- | 994 | IS_EL_CONV.doc |
|
- | rw-r--r-- | 203 | K.doc |
|
- | rw-r--r-- | 265 | KI.doc |
|
- | rw-r--r-- | 547 | LASTN_CONV.doc |
|
- | rw-r--r-- | 423 | LAST_CONV.doc |
|
- | rw-r--r-- | 625 | LEFT_AND_EXISTS_CONV.doc |
|
- | rw-r--r-- | 620 | LEFT_AND_FORALL_CONV.doc |
|
- | rw-r--r-- | 610 | LEFT_IMP_EXISTS_CONV.doc |
|
- | rw-r--r-- | 605 | LEFT_IMP_FORALL_CONV.doc |
|
- | rw-r--r-- | 619 | LEFT_OR_EXISTS_CONV.doc |
|
- | rw-r--r-- | 614 | LEFT_OR_FORALL_CONV.doc |
|
- | rw-r--r-- | 607 | LENGTH_CONV.doc |
|
- | rw-r--r-- | 795 | LIST_BETA_CONV.doc |
|
- | rw-r--r-- | 754 | LIST_CONJ.doc |
|
- | rw-r--r-- | 1,073 | LIST_INDUCT.doc |
|
- | rw-r--r-- | 1,120 | LIST_INDUCT_TAC.doc |
|
- | rw-r--r-- | 820 | LIST_MK_EXISTS.doc |
|
- | rw-r--r-- | 914 | LIST_MP.doc |
|
- | rw-r--r-- | 1,694 | MAP2_CONV.doc |
|
- | rw-r--r-- | 2,232 | MAP_CONV.doc |
|
- | rw-r--r-- | 1,046 | MAP_EVERY.doc |
|
- | rw-r--r-- | 955 | MAP_FIRST.doc |
|
- | rw-r--r-- | 952 | MATCH_ACCEPT_TAC.doc |
|
- | rw-r--r-- | 1,894 | MATCH_MP.doc |
|
- | rw-r--r-- | 1,175 | MATCH_MP_TAC.doc |
|
- | rw-r--r-- | 530 | MK_ABS.doc |
|
- | rw-r--r-- | 618 | MK_COMB.doc |
|
- | rw-r--r-- | 577 | MK_EXISTS.doc |
|
- | rw-r--r-- | 565 | ML_eval.doc |
|
- | rw-r--r-- | 595 | MP.doc |
|
- | rw-r--r-- | 493 | MP_TAC.doc |
|
- | rw-r--r-- | 693 | NEG_DISCH.doc |
|
- | rw-r--r-- | 413 | NOT_ELIM.doc |
|
- | rw-r--r-- | 485 | NOT_EQ_SYM.doc |
|
- | rw-r--r-- | 454 | NOT_EXISTS_CONV.doc |
|
- | rw-r--r-- | 509 | NOT_FORALL_CONV.doc |
|
- | rw-r--r-- | 448 | NOT_INTRO.doc |
|
- | rw-r--r-- | 1,300 | NOT_MP.doc |
|
- | rw-r--r-- | 164 | NO_CONV.doc |
|
- | rw-r--r-- | 264 | NO_TAC.doc |
|
- | rw-r--r-- | 481 | NO_THEN.doc |
|
- | rw-r--r-- | 1,085 | ONCE_ASM_REWRITE_RULE.doc |
|
- | rw-r--r-- | 1,613 | ONCE_ASM_REWRITE_TAC.doc |
|
- | rw-r--r-- | 2,712 | ONCE_DEPTH_CONV.doc |
|
- | rw-r--r-- | 799 | ONCE_REWRITE_CONV.doc |
|
- | rw-r--r-- | 857 | ONCE_REWRITE_RULE.doc |
|
- | rw-r--r-- | 1,669 | ONCE_REWRITE_TAC.doc |
|
- | rw-r--r-- | 2,380 | ONCE_REW_DEPTH_CONV.doc |
|
- | rw-r--r-- | 510 | ORELSE.doc |
|
- | rw-r--r-- | 484 | ORELSEC.doc |
|
- | rw-r--r-- | 587 | ORELSE_TCL.doc |
|
- | rw-r--r-- | 502 | OR_EXISTS_CONV.doc |
|
- | rw-r--r-- | 654 | OR_FORALL_CONV.doc |
|
- | rw-r--r-- | 2,988 | PAIRED_BETA_CONV.doc |
|
- | rw-r--r-- | 1,174 | PAIRED_ETA_CONV.doc |
|
- | rw-r--r-- | 1,176 | PART_MATCH.doc |
|
- | rw-r--r-- | 1,895 | POP_ASSUM.doc |
|
- | rw-r--r-- | 1,514 | POP_ASSUM_LIST.doc |
|
- | rw-r--r-- | 785 | PROVE.doc |
|
- | rw-r--r-- | 680 | PROVE_HYP.doc |
|
- | rw-r--r-- | 855 | PURE_ASM_REWRITE_RULE.doc |
|
- | rw-r--r-- | 987 | PURE_ASM_REWRITE_TAC.doc |
|
- | rw-r--r-- | 720 | PURE_ONCE_ASM_REWRITE_RULE.doc |
|
- | rw-r--r-- | 1,089 | PURE_ONCE_ASM_REWRITE_TAC.doc |
|
- | rw-r--r-- | 691 | PURE_ONCE_REWRITE_CONV.doc |
|
- | rw-r--r-- | 715 | PURE_ONCE_REWRITE_RULE.doc |
|
- | rw-r--r-- | 1,043 | PURE_ONCE_REWRITE_TAC.doc |
|
- | rw-r--r-- | 776 | PURE_REWRITE_CONV.doc |
|
- | rw-r--r-- | 906 | PURE_REWRITE_RULE.doc |
|
- | rw-r--r-- | 1,699 | PURE_REWRITE_TAC.doc |
|
- | rw-r--r-- | 910 | RAND_CONV.doc |
|
- | rw-r--r-- | 943 | RATOR_CONV.doc |
|
- | rw-r--r-- | 2,181 | REDEPTH_CONV.doc |
|
- | rw-r--r-- | 273 | REFL.doc |
|
- | rw-r--r-- | 477 | REFL_TAC.doc |
|
- | rw-r--r-- | 471 | REPEAT.doc |
|
- | rw-r--r-- | 721 | REPEATC.doc |
|
- | rw-r--r-- | 842 | REPEAT_GTCL.doc |
|
- | rw-r--r-- | 1,161 | REPEAT_TCL.doc |
|
- | rw-r--r-- | 4,268 | RES_CANON.doc |
|
- | rw-r--r-- | 2,394 | RES_TAC.doc |
|
- | rw-r--r-- | 3,031 | RES_THEN.doc |
|
- | rw-r--r-- | 661 | REVERSE_CONV.doc |
|
- | rw-r--r-- | 1,644 | REWRITE_CONV.doc |
|
- | rw-r--r-- | 1,827 | REWRITE_RULE.doc |
|
- | rw-r--r-- | 3,611 | REWRITE_TAC.doc |
|
- | rw-r--r-- | 5,748 | REWR_CONV.doc |
|
- | rw-r--r-- | 2,602 | REW_DEPTH_CONV.doc |
|
- | rw-r--r-- | 630 | RIGHT_AND_EXISTS_CONV.doc |
|
- | rw-r--r-- | 625 | RIGHT_AND_FORALL_CONV.doc |
|
- | rw-r--r-- | 613 | RIGHT_BETA.doc |
|
- | rw-r--r-- | 1,051 | RIGHT_CONV_RULE.doc |
|
- | rw-r--r-- | 614 | RIGHT_IMP_EXISTS_CONV.doc |
|
- | rw-r--r-- | 609 | RIGHT_IMP_FORALL_CONV.doc |
|
- | rw-r--r-- | 718 | RIGHT_LIST_BETA.doc |
|
- | rw-r--r-- | 624 | RIGHT_OR_EXISTS_CONV.doc |
|
- | rw-r--r-- | 619 | RIGHT_OR_FORALL_CONV.doc |
|
- | rw-r--r-- | 816 | RULE_ASSUM_TAC.doc |
|
- | rw-r--r-- | 1,262 | RecordStep.doc |
|
- | rw-r--r-- | 255 | S.doc |
|
- | rw-r--r-- | 1,457 | SCANL_CONV.doc |
|
- | rw-r--r-- | 1,459 | SCANR_CONV.doc |
|
- | rw-r--r-- | 760 | SEG_CONV.doc |
|
- | rw-r--r-- | 1,400 | SELECT_CONV.doc |
|
- | rw-r--r-- | 1,905 | SELECT_ELIM.doc |
|
- | rw-r--r-- | 913 | SELECT_EQ.doc |
|
- | rw-r--r-- | 978 | SELECT_INTRO.doc |
|
- | rw-r--r-- | 1,059 | SELECT_RULE.doc |
|
- | rw-r--r-- | 554 | SKOLEM_CONV.doc |
|
- | rw-r--r-- | 724 | SNOC_CONV.doc |
|
- | rw-r--r-- | 1,156 | SNOC_INDUCT_TAC.doc |
|
- | rw-r--r-- | 1,167 | SOME_EL_CONV.doc |
|
- | rw-r--r-- | 1,058 | SPEC.doc |
|
- | rw-r--r-- | 1,265 | SPECL.doc |
|
- | rw-r--r-- | 1,007 | SPEC_ALL.doc |
|
- | rw-r--r-- | 657 | SPEC_TAC.doc |
|
- | rw-r--r-- | 725 | SPEC_VAR.doc |
|
- | rw-r--r-- | 2,232 | STRIP_ASSUME_TAC.doc |
|
- | rw-r--r-- | 1,852 | STRIP_GOAL_THEN.doc |
|
- | rw-r--r-- | 1,854 | STRIP_TAC.doc |
|
- | rw-r--r-- | 2,305 | STRIP_THM_THEN.doc |
|
- | rw-r--r-- | 1,974 | STRUCT_CASES_TAC.doc |
|
- | rw-r--r-- | 1,330 | SUBGOAL_THEN.doc |
|
- | rw-r--r-- | 1,929 | SUBS.doc |
|
- | rw-r--r-- | 2,241 | SUBST.doc |
|
- | rw-r--r-- | 1,568 | SUBST1_TAC.doc |
|
- | rw-r--r-- | 1,687 | SUBST_ALL_TAC.doc |
|
- | rw-r--r-- | 2,242 | SUBST_CONV.doc |
|
- | rw-r--r-- | 1,796 | SUBST_MATCH.doc |
|
- | rw-r--r-- | 1,961 | SUBST_OCCS_TAC.doc |
|
- | rw-r--r-- | 1,754 | SUBST_TAC.doc |
|
- | rw-r--r-- | 1,562 | SUBS_OCCS.doc |
|
- | rw-r--r-- | 1,548 | SUB_CONV.doc |
|
- | rw-r--r-- | 432 | SWAP_EXISTS_CONV.doc |
|
- | rw-r--r-- | 393 | SYM.doc |
|
- | rw-r--r-- | 373 | SYM_CONV.doc |
|
- | rw-r--r-- | 653 | TAC_PROOF.doc |
|
- | rw-r--r-- | 923 | THEN.doc |
|
- | rw-r--r-- | 847 | THENC.doc |
|
- | rw-r--r-- | 816 | THENL.doc |
|
- | rw-r--r-- | 575 | THEN_TCL.doc |
|
- | rw-r--r-- | 1,259 | TOP_DEPTH_CONV.doc |
|
- | rw-r--r-- | 927 | TRANS.doc |
|
- | rw-r--r-- | 419 | TRY.doc |
|
- | rw-r--r-- | 600 | TRY_CONV.doc |
|
- | rw-r--r-- | 743 | UNDISCH.doc |
|
- | rw-r--r-- | 929 | UNDISCH_ALL.doc |
|
- | rw-r--r-- | 571 | UNDISCH_TAC.doc |
|
- | rw-r--r-- | 1,606 | VALID.doc |
|
- | rw-r--r-- | 223 | W.doc |
|
- | rw-r--r-- | 2,266 | X_CASES_THEN.doc |
|
- | rw-r--r-- | 2,446 | X_CASES_THENL.doc |
|
- | rw-r--r-- | 1,313 | X_CHOOSE_TAC.doc |
|
- | rw-r--r-- | 1,757 | X_CHOOSE_THEN.doc |
|
- | rw-r--r-- | 949 | X_FUN_EQ_CONV.doc |
|
- | rw-r--r-- | 672 | X_GEN_TAC.doc |
|
- | rw-r--r-- | 1,053 | X_SKOLEM_CONV.doc |
|
- | rw-r--r-- | 205 | abs_goals.doc |
|
- | rw-r--r-- | 214 | achieve_first.doc |
|
- | rw-r--r-- | 196 | achieves.doc |
|
- | rw-r--r-- | 444 | aconv.doc |
|
- | rw-r--r-- | 913 | activate_binders.doc |
|
- | rw-r--r-- | 959 | allowed_constant.doc |
|
- | rw-r--r-- | 368 | ancestors.doc |
|
- | rw-r--r-- | 427 | ancestry.doc |
|
- | rw-r--r-- | 268 | append.doc |
|
- | rw-r--r-- | 885 | append_openw.doc |
|
- | rw-r--r-- | 198 | apply_proof.doc |
|
- | rw-r--r-- | 220 | arb_term.doc |
|
- | rw-r--r-- | 330 | arity.doc |
|
- | rw-r--r-- | 420 | ascii.doc |
|
- | rw-r--r-- | 386 | ascii_code.doc |
|
- | rw-r--r-- | 500 | assert.doc |
|
- | rw-r--r-- | 1,209 | assignable_print_term.doc |
|
- | rw-r--r-- | 517 | assoc.doc |
|
- | rw-r--r-- | 2,185 | associate_restriction.doc |
|
- | rw-r--r-- | 217 | attempt_first.doc |
|
- | rw-r--r-- | 1,394 | autoload.doc |
|
- | rw-r--r-- | 1,090 | autoload_theory.doc |
|
- | rw-r--r-- | 851 | axiom.doc |
|
- | rw-r--r-- | 550 | axiom_lfn.doc |
|
- | rw-r--r-- | 772 | axiom_msg_lfn.doc |
|
- | rw-r--r-- | 996 | axioms.doc |
|
- | rw-r--r-- | 553 | b.doc |
|
- | rw-r--r-- | 1,843 | backup.doc |
|
- | rw-r--r-- | 1,120 | backup_limit.doc |
|
- | rw-r--r-- | 195 | backup_list.doc |
|
- | rw-r--r-- | 1,901 | basic_rewrites.doc |
|
- | rw-r--r-- | 650 | binders.doc |
|
- | rw-r--r-- | 235 | bndvar.doc |
|
- | rw-r--r-- | 219 | body.doc |
|
- | rw-r--r-- | 892 | bool_EQ_CONV.doc |
|
- | rw-r--r-- | 91 | bool_ty.doc |
|
- | rw-r--r-- | 275 | butlast.doc |
|
- | rw-r--r-- | 498 | cached_theories.doc |
|
- | rw-r--r-- | 337 | can.doc |
|
- | rw-r--r-- | 202 | change_state.doc |
|
- | rw-r--r-- | 196 | check_lhs.doc |
|
- | rw-r--r-- | 241 | check_specification.doc |
|
- | rw-r--r-- | 598 | check_valid.doc |
|
- | rw-r--r-- | 208 | check_varstruct.doc |
|
- | rw-r--r-- | 933 | chktac.doc |
|
- | rw-r--r-- | 418 | chop_list.doc |
|
- | rw-r--r-- | 520 | close.doc |
|
- | rw-r--r-- | 1,051 | close_theory.doc |
|
- | rw-r--r-- | 350 | com.doc |
|
- | rw-r--r-- | 356 | combine.doc |
|
- | rw-r--r-- | 3,215 | compile.doc |
|
- | rw-r--r-- | 743 | compilef.doc |
|
- | rw-r--r-- | 761 | compilet.doc |
|
- | rw-r--r-- | 1,375 | compiling.doc |
|
- | rw-r--r-- | 608 | compiling_stack.doc |
|
- | rw-r--r-- | 341 | concat.doc |
|
- | rw-r--r-- | 336 | concatl.doc |
|
- | rw-r--r-- | 228 | concl.doc |
|
- | rw-r--r-- | 1,089 | conjuncts.doc |
|
- | rw-r--r-- | 553 | constants.doc |
|
- | rw-r--r-- | 486 | current_theory.doc |
|
- | rw-r--r-- | 387 | curry.doc |
|
- | rw-r--r-- | 1,458 | define_finite_set_syntax.doc |
|
- | rw-r--r-- | 1,582 | define_load_lib_function.doc |
|
- | rw-r--r-- | 2,608 | define_new_type_bijections.doc |
|
- | rw-r--r-- | 1,033 | define_set_abstraction_syntax.doc |
|
- | rw-r--r-- | 4,921 | define_type.doc |
|
- | rw-r--r-- | 944 | definition.doc |
|
- | rw-r--r-- | 630 | definition_lfn.doc |
|
- | rw-r--r-- | 849 | definition_msg_lfn.doc |
|
- | rw-r--r-- | 1,157 | definitions.doc |
|
- | rw-r--r-- | 372 | delete_cache.doc |
|
- | rw-r--r-- | 1,182 | delete_thm.doc |
|
- | rw-r--r-- | 379 | dest_abs.doc |
|
- | rw-r--r-- | 406 | dest_comb.doc |
|
- | rw-r--r-- | 367 | dest_cond.doc |
|
- | rw-r--r-- | 263 | dest_conj.doc |
|
- | rw-r--r-- | 487 | dest_cons.doc |
|
- | rw-r--r-- | 376 | dest_const.doc |
|
- | rw-r--r-- | 203 | dest_definition.doc |
|
- | rw-r--r-- | 345 | dest_disj.doc |
|
- | rw-r--r-- | 244 | dest_eq.doc |
|
- | rw-r--r-- | 417 | dest_exists.doc |
|
- | rw-r--r-- | 409 | dest_forall.doc |
|
- | rw-r--r-- | 191 | dest_form.doc |
|
- | rw-r--r-- | 522 | dest_imp.doc |
|
- | rw-r--r-- | 497 | dest_let.doc |
|
- | rw-r--r-- | 366 | dest_list.doc |
|
- | rw-r--r-- | 288 | dest_neg.doc |
|
- | rw-r--r-- | 678 | dest_neg_imp.doc |
|
- | rw-r--r-- | 414 | dest_pabs.doc |
|
- | rw-r--r-- | 321 | dest_pair.doc |
|
- | rw-r--r-- | 436 | dest_pred.doc |
|
- | rw-r--r-- | 369 | dest_select.doc |
|
- | rw-r--r-- | 307 | dest_thm.doc |
|
- | rw-r--r-- | 536 | dest_type.doc |
|
- | rw-r--r-- | 298 | dest_var.doc |
|
- | rw-r--r-- | 469 | dest_vartype.doc |
|
- | rw-r--r-- | 391 | disch.doc |
|
- | rw-r--r-- | 1,070 | disjuncts.doc |
|
- | rw-r--r-- | 266 | distinct.doc |
|
- | rw-r--r-- | 891 | do.doc |
|
- | rw-r--r-- | 555 | draft_mode.doc |
|
- | rw-r--r-- | 1,188 | dropout.doc |
|
- | rw-r--r-- | 522 | e.doc |
|
- | rw-r--r-- | 375 | el.doc |
|
- | rw-r--r-- | 439 | end_itlist.doc |
|
- | rw-r--r-- | 218 | enter_form_rep.doc |
|
- | rw-r--r-- | 219 | enter_term.doc |
|
- | rw-r--r-- | 218 | enter_term_rep.doc |
|
- | rw-r--r-- | 434 | exists.doc |
|
- | rw-r--r-- | 3,213 | expand.doc |
|
- | rw-r--r-- | 2,609 | expandf.doc |
|
- | rw-r--r-- | 466 | explode.doc |
|
- | rw-r--r-- | 2,404 | extend_theory.doc |
|
- | rw-r--r-- | 91 | falsity.doc |
|
- | rw-r--r-- | 1,070 | fast_arith.doc |
|
- | rw-r--r-- | 384 | filter.doc |
|
- | rw-r--r-- | 430 | find.doc |
|
- | rw-r--r-- | 594 | find_file.doc |
|
- | rw-r--r-- | 1,118 | find_match.doc |
|
- | rw-r--r-- | 827 | find_ml_file.doc |
|
- | rw-r--r-- | 519 | find_term.doc |
|
- | rw-r--r-- | 588 | find_terms.doc |
|
- | rw-r--r-- | 588 | find_theory.doc |
|
- | rw-r--r-- | 368 | flags.doc |
|
- | rw-r--r-- | 337 | flat.doc |
|
- | rw-r--r-- | 421 | forall.doc |
|
- | rw-r--r-- | 757 | free_in.doc |
|
- | rw-r--r-- | 547 | frees.doc |
|
- | rw-r--r-- | 615 | freesl.doc |
|
- | rw-r--r-- | 180 | fst.doc |
|
- | rw-r--r-- | 1,147 | funpow.doc |
|
- | rw-r--r-- | 657 | g.doc |
|
- | rw-r--r-- | 984 | genvar.doc |
|
- | rw-r--r-- | 423 | get_const_type.doc |
|
- | rw-r--r-- | 449 | get_flag_value.doc |
|
- | rw-r--r-- | 1,353 | get_state.doc |
|
- | rw-r--r-- | 2,100 | get_steps.doc |
|
- | rw-r--r-- | 197 | get_type.doc |
|
- | rw-r--r-- | 485 | getenv.doc |
|
- | rw-r--r-- | 178 | goals.doc |
|
- | rw-r--r-- | 219 | hd.doc |
|
- | rw-r--r-- | 704 | help.doc |
|
- | rw-r--r-- | 816 | help_search_path.doc |
|
- | rw-r--r-- | 646 | hide_constant.doc |
|
- | rw-r--r-- | 400 | hol_pathname.doc |
|
- | rw-r--r-- | 990 | host_name.doc |
|
- | rw-r--r-- | 268 | hyp.doc |
|
- | rw-r--r-- | 637 | hyp_union.doc |
|
- | rw-r--r-- | 599 | implode.doc |
|
- | rw-r--r-- | 678 | infix_variable.doc |
|
- | rw-r--r-- | 879 | infixes.doc |
|
- | rw-r--r-- | 620 | inject_input.doc |
|
- | rw-r--r-- | 483 | inl.doc |
|
- | rw-r--r-- | 475 | inr.doc |
|
- | rw-r--r-- | 1,262 | inst.doc |
|
- | rw-r--r-- | 876 | inst_check.doc |
|
- | rw-r--r-- | 924 | inst_rename_list.doc |
|
- | rw-r--r-- | 1,108 | inst_type.doc |
|
- | rw-r--r-- | 980 | install.doc |
|
- | rw-r--r-- | 482 | int_of_string.doc |
|
- | rw-r--r-- | 387 | int_of_term.doc |
|
- | rw-r--r-- | 395 | interface_map.doc |
|
- | rw-r--r-- | 441 | intersect.doc |
|
- | rw-r--r-- | 291 | is_abs.doc |
|
- | rw-r--r-- | 596 | is_alphanum.doc |
|
- | rw-r--r-- | 566 | is_axiom.doc |
|
- | rw-r--r-- | 434 | is_binder.doc |
|
- | rw-r--r-- | 740 | is_binder_type.doc |
|
- | rw-r--r-- | 313 | is_comb.doc |
|
- | rw-r--r-- | 272 | is_cond.doc |
|
- | rw-r--r-- | 268 | is_conj.doc |
|
- | rw-r--r-- | 311 | is_cons.doc |
|
- | rw-r--r-- | 292 | is_const.doc |
|
- | rw-r--r-- | 514 | is_constant.doc |
|
- | rw-r--r-- | 199 | is_definition.doc |
|
- | rw-r--r-- | 268 | is_disj.doc |
|
- | rw-r--r-- | 253 | is_eq.doc |
|
- | rw-r--r-- | 309 | is_exists.doc |
|
- | rw-r--r-- | 303 | is_forall.doc |
|
- | rw-r--r-- | 603 | is_hidden.doc |
|
- | rw-r--r-- | 439 | is_imp.doc |
|
- | rw-r--r-- | 406 | is_infix.doc |
|
- | rw-r--r-- | 699 | is_infix_type.doc |
|
- | rw-r--r-- | 410 | is_let.doc |
|
- | rw-r--r-- | 545 | is_letter.doc |
|
- | rw-r--r-- | 283 | is_list.doc |
|
- | rw-r--r-- | 388 | is_ml_curried_infix.doc |
|
- | rw-r--r-- | 373 | is_ml_infix.doc |
|
- | rw-r--r-- | 383 | is_ml_paired_infix.doc |
|
- | rw-r--r-- | 251 | is_neg.doc |
|
- | rw-r--r-- | 520 | is_neg_imp.doc |
|
- | rw-r--r-- | 327 | is_pabs.doc |
|
- | rw-r--r-- | 253 | is_pair.doc |
|
- | rw-r--r-- | 396 | is_pred.doc |
|
- | rw-r--r-- | 1,080 | is_recording_proof.doc |
|
- | rw-r--r-- | 282 | is_select.doc |
|
- | rw-r--r-- | 268 | is_type.doc |
|
- | rw-r--r-- | 282 | is_var.doc |
|
- | rw-r--r-- | 411 | is_vartype.doc |
|
- | rw-r--r-- | 209 | isl.doc |
|
- | rw-r--r-- | 423 | it.doc |
|
- | rw-r--r-- | 432 | itlist.doc |
|
- | rw-r--r-- | 553 | itlist2.doc |
|
- | rw-r--r-- | 228 | last.doc |
|
- | rw-r--r-- | 171 | length.doc |
|
- | rw-r--r-- | 2,928 | let_CONV.doc |
|
- | rw-r--r-- | 996 | let_after.doc |
|
- | rw-r--r-- | 967 | let_before.doc |
|
- | rw-r--r-- | 228 | lhs.doc |
|
- | rw-r--r-- | 263 | libraries.doc |
|
- | rw-r--r-- | 5,591 | library_loader.doc |
|
- | rw-r--r-- | 1,159 | library_pathname.doc |
|
- | rw-r--r-- | 795 | library_search_path.doc |
|
- | rw-r--r-- | 767 | link.doc |
|
- | rw-r--r-- | 922 | lisp.doc |
|
- | rw-r--r-- | 439 | lisp_dir_pathname.doc |
|
- | rw-r--r-- | 1,598 | list_EQ_CONV.doc |
|
- | rw-r--r-- | 1,544 | list_FOLD_CONV.doc |
|
- | rw-r--r-- | 363 | list_mk_abs.doc |
|
- | rw-r--r-- | 645 | list_mk_comb.doc |
|
- | rw-r--r-- | 542 | list_mk_conj.doc |
|
- | rw-r--r-- | 542 | list_mk_disj.doc |
|
- | rw-r--r-- | 531 | list_mk_exists.doc |
|
- | rw-r--r-- | 530 | list_mk_forall.doc |
|
- | rw-r--r-- | 682 | list_mk_imp.doc |
|
- | rw-r--r-- | 372 | list_mk_pair.doc |
|
- | rw-r--r-- | 433 | list_of_binders.doc |
|
- | rw-r--r-- | 806 | load.doc |
|
- | rw-r--r-- | 713 | load_axiom.doc |
|
- | rw-r--r-- | 781 | load_axioms.doc |
|
- | rw-r--r-- | 767 | load_definition.doc |
|
- | rw-r--r-- | 747 | load_definitions.doc |
|
- | rw-r--r-- | 2,202 | load_library.doc |
|
- | rw-r--r-- | 707 | load_theorem.doc |
|
- | rw-r--r-- | 772 | load_theorems.doc |
|
- | rw-r--r-- | 1,110 | load_theory.doc |
|
- | rw-r--r-- | 757 | loadf.doc |
|
- | rw-r--r-- | 807 | loadt.doc |
|
- | rw-r--r-- | 216 | lookup_form_rep.doc |
|
- | rw-r--r-- | 211 | lookup_term.doc |
|
- | rw-r--r-- | 216 | lookup_term_rep.doc |
|
- | rw-r--r-- | 917 | lsp.doc |
|
- | rw-r--r-- | 307 | map.doc |
|
- | rw-r--r-- | 401 | map2.doc |
|
- | rw-r--r-- | 358 | mapfilter.doc |
|
- | rw-r--r-- | 916 | maptok.doc |
|
- | rw-r--r-- | 1,682 | match.doc |
|
- | rw-r--r-- | 770 | max_print_depth.doc |
|
- | rw-r--r-- | 314 | mem.doc |
|
- | rw-r--r-- | 216 | merge_nets_rep.doc |
|
- | rw-r--r-- | 229 | merge_term_nets.doc |
|
- | rw-r--r-- | 583 | message.doc |
|
- | rw-r--r-- | 299 | mk_abs.doc |
|
- | rw-r--r-- | 438 | mk_comb.doc |
|
- | rw-r--r-- | 313 | mk_cond.doc |
|
- | rw-r--r-- | 281 | mk_conj.doc |
|
- | rw-r--r-- | 362 | mk_cons.doc |
|
- | rw-r--r-- | 627 | mk_const.doc |
|
- | rw-r--r-- | 231 | mk_conv_net.doc |
|
- | rw-r--r-- | 199 | mk_definition.doc |
|
- | rw-r--r-- | 281 | mk_disj.doc |
|
- | rw-r--r-- | 241 | mk_eq.doc |
|
- | rw-r--r-- | 328 | mk_exists.doc |
|
- | rw-r--r-- | 333 | mk_forall.doc |
|
- | rw-r--r-- | 187 | mk_form.doc |
|
- | rw-r--r-- | 276 | mk_imp.doc |
|
- | rw-r--r-- | 546 | mk_let.doc |
|
- | rw-r--r-- | 445 | mk_list.doc |
|
- | rw-r--r-- | 216 | mk_neg.doc |
|
- | rw-r--r-- | 334 | mk_pabs.doc |
|
- | rw-r--r-- | 247 | mk_pair.doc |
|
- | rw-r--r-- | 204 | mk_pp_thm.doc |
|
- | rw-r--r-- | 494 | mk_pred.doc |
|
- | rw-r--r-- | 634 | mk_primed_var.doc |
|
- | rw-r--r-- | 296 | mk_select.doc |
|
- | rw-r--r-- | 1,514 | mk_thm.doc |
|
- | rw-r--r-- | 660 | mk_type.doc |
|
- | rw-r--r-- | 472 | mk_var.doc |
|
- | rw-r--r-- | 534 | mk_vartype.doc |
|
- | rw-r--r-- | 755 | ml_curried_infix.doc |
|
- | rw-r--r-- | 429 | ml_dir_pathname.doc |
|
- | rw-r--r-- | 785 | ml_paired_infix.doc |
|
- | rw-r--r-- | 231 | n_strip_quant.doc |
|
- | rw-r--r-- | 1,145 | new_alphanum.doc |
|
- | rw-r--r-- | 1,083 | new_axiom.doc |
|
- | rw-r--r-- | 774 | new_binder.doc |
|
- | rw-r--r-- | 3,111 | new_binder_definition.doc |
|
- | rw-r--r-- | 709 | new_constant.doc |
|
- | rw-r--r-- | 2,329 | new_definition.doc |
|
- | rw-r--r-- | 644 | new_flag.doc |
|
- | rw-r--r-- | 2,625 | new_gen_definition.doc |
|
- | rw-r--r-- | 991 | new_infix.doc |
|
- | rw-r--r-- | 2,953 | new_infix_definition.doc |
|
- | rw-r--r-- | 2,962 | new_infix_list_rec_definition.doc |
|
- | rw-r--r-- | 2,936 | new_infix_prim_rec_definition.doc |
|
- | rw-r--r-- | 1,014 | new_letter.doc |
|
- | rw-r--r-- | 3,314 | new_list_rec_definition.doc |
|
- | rw-r--r-- | 211 | new_open_axiom.doc |
|
- | rw-r--r-- | 1,411 | new_parent.doc |
|
- | rw-r--r-- | 449 | new_predicate.doc |
|
- | rw-r--r-- | 3,604 | new_prim_rec_definition.doc |
|
- | rw-r--r-- | 6,302 | new_recursive_definition.doc |
|
- | rw-r--r-- | 1,158 | new_special_symbol.doc |
|
- | rw-r--r-- | 2,578 | new_specification.doc |
|
- | rw-r--r-- | 200 | new_stack.doc |
|
- | rw-r--r-- | 1,222 | new_syntax_block.doc |
|
- | rw-r--r-- | 2,570 | new_theory.doc |
|
- | rw-r--r-- | 827 | new_type.doc |
|
- | rw-r--r-- | 1,048 | new_type_abbrev.doc |
|
- | rw-r--r-- | 1,861 | new_type_definition.doc |
|
- | rw-r--r-- | 193 | nil_term_net.doc |
|
- | rw-r--r-- | 283 | not.doc |
|
- | rw-r--r-- | 249 | null.doc |
|
- | rw-r--r-- | 631 | num_CONV.doc |
|
- | rw-r--r-- | 1,080 | num_EQ_CONV.doc |
|
- | rw-r--r-- | 220 | o.doc |
|
- | rw-r--r-- | 277 | oo.doc |
|
- | rw-r--r-- | 562 | openi.doc |
|
- | rw-r--r-- | 645 | openw.doc |
|
- | rw-r--r-- | 459 | outl.doc |
|
- | rw-r--r-- | 463 | outr.doc |
|
- | rw-r--r-- | 523 | p.doc |
|
- | rw-r--r-- | 196 | pair.doc |
|
- | rw-r--r-- | 219 | paired_delete_thm.doc |
|
- | rw-r--r-- | 213 | paired_new_type.doc |
|
- | rw-r--r-- | 213 | paired_theorem.doc |
|
- | rw-r--r-- | 1,354 | parents.doc |
|
- | rw-r--r-- | 1,001 | parse_as_binder.doc |
|
- | rw-r--r-- | 471 | partition.doc |
|
- | rw-r--r-- | 211 | pop_proofs.doc |
|
- | rw-r--r-- | 223 | pop_proofs_print.doc |
|
- | rw-r--r-- | 200 | pp_axiom.doc |
|
- | rw-r--r-- | 993 | preterm_abs.doc |
|
- | rw-r--r-- | 689 | preterm_antiquot.doc |
|
- | rw-r--r-- | 770 | preterm_comb.doc |
|
- | rw-r--r-- | 699 | preterm_const.doc |
|
- | rw-r--r-- | 564 | preterm_to_term.doc |
|
- | rw-r--r-- | 773 | preterm_typed.doc |
|
- | rw-r--r-- | 846 | preterm_var.doc |
|
- | rw-r--r-- | 806 | print_all_thm.doc |
|
- | rw-r--r-- | 1,819 | print_begin.doc |
|
- | rw-r--r-- | 386 | print_bool.doc |
|
- | rw-r--r-- | 1,522 | print_break.doc |
|
- | rw-r--r-- | 499 | print_defined_types.doc |
|
- | rw-r--r-- | 578 | print_end.doc |
|
- | rw-r--r-- | 620 | print_goal.doc |
|
- | rw-r--r-- | 198 | print_hyps.doc |
|
- | rw-r--r-- | 1,404 | print_ibegin.doc |
|
- | rw-r--r-- | 546 | print_int.doc |
|
- | rw-r--r-- | 1,207 | print_list.doc |
|
- | rw-r--r-- | 574 | print_newline.doc |
|
- | rw-r--r-- | 211 | print_stack.doc |
|
- | rw-r--r-- | 1,379 | print_state.doc |
|
- | rw-r--r-- | 670 | print_string.doc |
|
- | rw-r--r-- | 205 | print_subgoals.doc |
|
- | rw-r--r-- | 566 | print_term.doc |
|
- | rw-r--r-- | 799 | print_theory.doc |
|
- | rw-r--r-- | 704 | print_thm.doc |
|
- | rw-r--r-- | 655 | print_tok.doc |
|
- | rw-r--r-- | 552 | print_type.doc |
|
- | rw-r--r-- | 687 | print_unquoted_term.doc |
|
- | rw-r--r-- | 732 | print_unquoted_type.doc |
|
- | rw-r--r-- | 513 | print_void.doc |
|
- | rw-r--r-- | 342 | prompt.doc |
|
- | rw-r--r-- | 867 | prove.doc |
|
- | rw-r--r-- | 727 | prove_abs_fn_one_one.doc |
|
- | rw-r--r-- | 655 | prove_abs_fn_onto.doc |
|
- | rw-r--r-- | 1,251 | prove_cases_thm.doc |
|
- | rw-r--r-- | 1,427 | prove_constructors_distinct.doc |
|
- | rw-r--r-- | 1,516 | prove_constructors_one_one.doc |
|
- | rw-r--r-- | 1,568 | prove_induction_thm.doc |
|
- | rw-r--r-- | 1,710 | prove_rec_fn_exists.doc |
|
- | rw-r--r-- | 683 | prove_rep_fn_one_one.doc |
|
- | rw-r--r-- | 692 | prove_rep_fn_onto.doc |
|
- | rw-r--r-- | 1,191 | prove_thm.doc |
|
- | rw-r--r-- | 229 | push_fsubgoals.doc |
|
- | rw-r--r-- | 223 | push_print.doc |
|
- | rw-r--r-- | 227 | push_subgoals.doc |
|
- | rw-r--r-- | 140 | quit.doc |
|
- | rw-r--r-- | 535 | r.doc |
|
- | rw-r--r-- | 252 | rand.doc |
|
- | rw-r--r-- | 257 | rator.doc |
|
- | rw-r--r-- | 1,175 | read.doc |
|
- | rw-r--r-- | 2,176 | record_proof.doc |
|
- | rw-r--r-- | 408 | remove.doc |
|
- | rw-r--r-- | 609 | remove_sticky_type.doc |
|
- | rw-r--r-- | 205 | rep_goals.doc |
|
- | rw-r--r-- | 283 | replicate.doc |
|
- | rw-r--r-- | 1,312 | resume_recording.doc |
|
- | rw-r--r-- | 172 | rev.doc |
|
- | rw-r--r-- | 530 | rev_assoc.doc |
|
- | rw-r--r-- | 427 | rev_itlist.doc |
|
- | rw-r--r-- | 225 | rhs.doc |
|
- | rw-r--r-- | 183 | root_goal.doc |
|
- | rw-r--r-- | 1,852 | rotate.doc |
|
- | rw-r--r-- | 205 | rotate_goals.doc |
|
- | rw-r--r-- | 218 | rotate_top.doc |
|
- | rw-r--r-- | 910 | save.doc |
|
- | rw-r--r-- | 1,551 | save_thm.doc |
|
- | rw-r--r-- | 2,129 | save_top_thm.doc |
|
- | rw-r--r-- | 1,206 | search_path.doc |
|
- | rw-r--r-- | 432 | set_equal.doc |
|
- | rw-r--r-- | 868 | set_fail.doc |
|
- | rw-r--r-- | 702 | set_fail_prefix.doc |
|
- | rw-r--r-- | 467 | set_flag.doc |
|
- | rw-r--r-- | 2,749 | set_goal.doc |
|
- | rw-r--r-- | 642 | set_help.doc |
|
- | rw-r--r-- | 828 | set_help_search_path.doc |
|
- | rw-r--r-- | 1,423 | set_interface_map.doc |
|
- | rw-r--r-- | 724 | set_lambda.doc |
|
- | rw-r--r-- | 1,256 | set_library_search_path.doc |
|
- | rw-r--r-- | 870 | set_margin.doc |
|
- | rw-r--r-- | 484 | set_pretty_mode.doc |
|
- | rw-r--r-- | 730 | set_prompt.doc |
|
- | rw-r--r-- | 1,430 | set_search_path.doc |
|
- | rw-r--r-- | 1,358 | set_state.doc |
|
- | rw-r--r-- | 1,178 | set_sticky_type.doc |
|
- | rw-r--r-- | 481 | set_string_escape.doc |
|
- | rw-r--r-- | 419 | set_thm_count.doc |
|
- | rw-r--r-- | 709 | set_turnstile.doc |
|
- | rw-r--r-- | 522 | setify.doc |
|
- | rw-r--r-- | 1,101 | show_types.doc |
|
- | rw-r--r-- | 182 | snd.doc |
|
- | rw-r--r-- | 956 | sort.doc |
|
- | rw-r--r-- | 714 | special_symbols.doc |
|
- | rw-r--r-- | 275 | split.doc |
|
- | rw-r--r-- | 439 | splitp.doc |
|
- | rw-r--r-- | 552 | sticky_list.doc |
|
- | rw-r--r-- | 203 | store_binders.doc |
|
- | rw-r--r-- | 215 | store_definition.doc |
|
- | rw-r--r-- | 396 | string_of_int.doc |
|
- | rw-r--r-- | 375 | strip_abs.doc |
|
- | rw-r--r-- | 544 | strip_comb.doc |
|
- | rw-r--r-- | 426 | strip_exists.doc |
|
- | rw-r--r-- | 421 | strip_forall.doc |
|
- | rw-r--r-- | 472 | strip_imp.doc |
|
- | rw-r--r-- | 616 | strip_pair.doc |
|
- | rw-r--r-- | 927 | subst.doc |
|
- | rw-r--r-- | 1,032 | subst_occs.doc |
|
- | rw-r--r-- | 444 | subtract.doc |
|
- | rw-r--r-- | 1,492 | suspend_recording.doc |
|
- | rw-r--r-- | 353 | syserror.doc |
|
- | rw-r--r-- | 400 | system.doc |
|
- | rw-r--r-- | 474 | term_of_int.doc |
|
- | rw-r--r-- | 897 | theorem.doc |
|
- | rw-r--r-- | 577 | theorem_lfn.doc |
|
- | rw-r--r-- | 819 | theorem_msg_lfn.doc |
|
- | rw-r--r-- | 1,018 | theorems.doc |
|
- | rw-r--r-- | 379 | thm_count.doc |
|
- | rw-r--r-- | 623 | thm_frees.doc |
|
- | rw-r--r-- | 1,051 | timer.doc |
|
- | rw-r--r-- | 256 | tl.doc |
|
- | rw-r--r-- | 699 | top_goal.doc |
|
- | rw-r--r-- | 1,688 | top_print.doc |
|
- | rw-r--r-- | 199 | top_proof.doc |
|
- | rw-r--r-- | 888 | top_thm.doc |
|
- | rw-r--r-- | 523 | tryfind.doc |
|
- | rw-r--r-- | 929 | tty_read.doc |
|
- | rw-r--r-- | 472 | tty_write.doc |
|
- | rw-r--r-- | 680 | type_abbrevs.doc |
|
- | rw-r--r-- | 482 | type_in.doc |
|
- | rw-r--r-- | 485 | type_in_type.doc |
|
- | rw-r--r-- | 161 | type_of.doc |
|
- | rw-r--r-- | 423 | type_tyvars.doc |
|
- | rw-r--r-- | 1,013 | types.doc |
|
- | rw-r--r-- | 554 | tyvars.doc |
|
- | rw-r--r-- | 651 | tyvarsl.doc |
|
- | rw-r--r-- | 322 | uncurry.doc |
|
- | rw-r--r-- | 675 | undo_autoload.doc |
|
- | rw-r--r-- | 645 | unhide_constant.doc |
|
- | rw-r--r-- | 454 | union.doc |
|
- | rw-r--r-- | 623 | unlink.doc |
|
- | rw-r--r-- | 1,354 | variant.doc |
|
- | rw-r--r-- | 369 | vars.doc |
|
- | rw-r--r-- | 407 | varsl.doc |
|
- | rw-r--r-- | 463 | version.doc |
|
- | rw-r--r-- | 508 | word_separators.doc |
|
- | rw-r--r-- | 769 | words.doc |
|
- | rw-r--r-- | 878 | words2.doc |
|
- | rw-r--r-- | 1,021 | write.doc |