package info
(click to toggle)
hol88 2.02.19940316-1
- links: PTS
- area: main
- in suites: etch, etch-m68k
- size: 63,052 kB
- ctags: 19,365
- sloc: ml: 199,939; ansic: 9,300; sh: 7,118; makefile: 6,076; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
Folder: entries
 |
.. (parent) | |||
 |
- | rw-r--r-- | 809 | ADD_SUPPOSE.doc |
|
- | rw-r--r-- | 723 | ADD_THEOREM.doc |
|
- | rw-r--r-- | 512 | ALL_STACKS.doc |
|
- | rw-r--r-- | 321 | APPLY_TRANSFORM.doc |
|
- | rw-r--r-- | 686 | ASM_REWRITE_WIN.doc |
|
- | rw-r--r-- | 683 | BAD_CONJECTURES.doc |
|
- | rw-r--r-- | 666 | BEGIN_STACK.doc |
|
- | rw-r--r-- | 1,540 | BEGIN_STACK_TAC.doc |
|
- | rw-r--r-- | 903 | CLOSE_WIN.doc |
|
- | rw-r--r-- | 483 | CONJECTURE.doc |
|
- | rw-r--r-- | 762 | CONVERT_WIN.doc |
|
- | rw-r--r-- | 263 | CURRENT_NAME.doc |
|
- | rw-r--r-- | 441 | END_STACK.doc |
|
- | rw-r--r-- | 1,321 | END_STACK_TAC.doc |
|
- | rw-r--r-- | 1,155 | ESTABLISH.doc |
|
- | rw-r--r-- | 749 | EXISTS_PMI.doc |
|
- | rw-r--r-- | 1,053 | FILTER_ASM_REWRITE_WIN.doc |
|
- | rw-r--r-- | 874 | FILTER_ONCE_ASM_REWRITE_WIN.doc |
|
- | rw-r--r-- | 1,045 | FILTER_PURE_ASM_REWRITE_WIN.doc |
|
- | rw-r--r-- | 927 | FILTER_PURE_ONCE_ASM_REWRITE_WIN.doc |
|
- | rw-r--r-- | 206 | FOCUS.doc |
|
- | rw-r--r-- | 940 | FOC_RULE_WIN.doc |
|
- | rw-r--r-- | 689 | GEN_OPEN_WIN.doc |
|
- | rw-r--r-- | 2,896 | GEN_REWRITE_WIN.doc |
|
- | rw-r--r-- | 209 | GET_MAX_HIST.doc |
|
- | rw-r--r-- | 304 | IMP_PMI.doc |
|
- | rw-r--r-- | 341 | IMP_PMI_CONV.doc |
|
- | rw-r--r-- | 215 | IMP_REFL.doc |
|
- | rw-r--r-- | 237 | LEMMA_THMS.doc |
|
- | rw-r--r-- | 974 | MATCH_TRANSFORM_WIN.doc |
|
- | rw-r--r-- | 622 | ONCE_ASM_REWRITE_WIN.doc |
|
- | rw-r--r-- | 601 | ONCE_REWRITE_WIN.doc |
|
- | rw-r--r-- | 1,432 | OPEN_CONTEXT.doc |
|
- | rw-r--r-- | 839 | OPEN_WIN.doc |
|
- | rw-r--r-- | 311 | PMI_IMP.doc |
|
- | rw-r--r-- | 349 | PMI_IMP_CONV.doc |
|
- | rw-r--r-- | 233 | PMI_REFL.doc |
|
- | rw-r--r-- | 303 | PMI_TRANS.doc |
|
- | rw-r--r-- | 820 | PRINT_STACK.doc |
|
- | rw-r--r-- | 704 | PURE_ASM_REWRITE_WIN.doc |
|
- | rw-r--r-- | 619 | PURE_ONCE_ASM_REWRITE_WIN.doc |
|
- | rw-r--r-- | 595 | PURE_ONCE_REWRITE_WIN.doc |
|
- | rw-r--r-- | 718 | PURE_REWRITE_WIN.doc |
|
- | rw-r--r-- | 591 | REDO.doc |
|
- | rw-r--r-- | 713 | REWRITE_WIN.doc |
|
- | rw-r--r-- | 821 | RULE_WIN.doc |
|
- | rw-r--r-- | 573 | SAVE_WIN_THM.doc |
|
- | rw-r--r-- | 236 | SET_MAX_HIST.doc |
|
- | rw-r--r-- | 339 | SET_STACK.doc |
|
- | rw-r--r-- | 946 | SMASH.doc |
|
- | rw-r--r-- | 873 | TACTIC_WIN.doc |
|
- | rw-r--r-- | 945 | THM_RULE_WIN.doc |
|
- | rw-r--r-- | 143 | TOP_WIN.doc |
|
- | rw-r--r-- | 818 | TRANSFORM_WIN.doc |
|
- | rw-r--r-- | 710 | UNDO.doc |
|
- | rw-r--r-- | 395 | UNDO_WIN.doc |
|
- | rw-r--r-- | 517 | WIN_THM.doc |
|
- | rw-r--r-- | 933 | add_relation.doc |
|
- | rw-r--r-- | 774 | add_suppose.doc |
|
- | rw-r--r-- | 685 | add_theorem.doc |
|
- | rw-r--r-- | 1,739 | add_weak.doc |
|
- | rw-r--r-- | 683 | all_hypotheses.doc |
|
- | rw-r--r-- | 716 | asm_rewrite_win.doc |
|
- | rw-r--r-- | 638 | bound.doc |
|
- | rw-r--r-- | 428 | conjecture.doc |
|
- | rw-r--r-- | 497 | conjectures.doc |
|
- | rw-r--r-- | 313 | context.doc |
|
- | rw-r--r-- | 594 | convert_win.doc |
|
- | rw-r--r-- | 402 | create_win.doc |
|
- | rw-r--r-- | 469 | dest_pmi.doc |
|
- | rw-r--r-- | 647 | disp_hypotheses.doc |
|
- | rw-r--r-- | 713 | empty_rules.doc |
|
- | rw-r--r-- | 151 | equiv_tm.doc |
|
- | rw-r--r-- | 868 | establish.doc |
|
- | rw-r--r-- | 991 | filter_asm_rewrite_win.doc |
|
- | rw-r--r-- | 875 | filter_once_asm_rewrite_win.doc |
|
- | rw-r--r-- | 978 | filter_pure_asm_rewrite_win.doc |
|
- | rw-r--r-- | 863 | filter_pure_once_asm_rewrite_win.doc |
|
- | rw-r--r-- | 967 | foc_rule_win.doc |
|
- | rw-r--r-- | 131 | focus.doc |
|
- | rw-r--r-- | 708 | gen_open_win.doc |
|
- | rw-r--r-- | 2,894 | gen_rewrite_win.doc |
|
- | rw-r--r-- | 616 | hyp_thms.doc |
|
- | rw-r--r-- | 712 | hypotheses.doc |
|
- | rw-r--r-- | 128 | imp_tm.doc |
|
- | rw-r--r-- | 399 | is_pmi.doc |
|
- | rw-r--r-- | 293 | is_trueimp.doc |
|
- | rw-r--r-- | 211 | lemma_thms.doc |
|
- | rw-r--r-- | 417 | lemmas.doc |
|
- | rw-r--r-- | 715 | load_window.doc |
|
- | rw-r--r-- | 964 | match_transform_win.doc |
|
- | rw-r--r-- | 628 | once_asm_rewrite_win.doc |
|
- | rw-r--r-- | 622 | once_rewrite_win.doc |
|
- | rw-r--r-- | 1,211 | open_TAC.doc |
|
- | rw-r--r-- | 1,106 | open_context.doc |
|
- | rw-r--r-- | 871 | open_win.doc |
|
- | rw-r--r-- | 139 | origin.doc |
|
- | rw-r--r-- | 128 | pmi_tm.doc |
|
- | rw-r--r-- | 713 | pure_asm_rewrite_win.doc |
|
- | rw-r--r-- | 639 | pure_once_asm_rewrite_win.doc |
|
- | rw-r--r-- | 616 | pure_once_rewrite_win.doc |
|
- | rw-r--r-- | 701 | pure_rewrite_win.doc |
|
- | rw-r--r-- | 249 | relation.doc |
|
- | rw-r--r-- | 692 | rewrite_win.doc |
|
- | rw-r--r-- | 754 | rule_win.doc |
|
- | rw-r--r-- | 354 | store_rule.doc |
|
- | rw-r--r-- | 269 | suppositions.doc |
|
- | rw-r--r-- | 785 | tactic_win.doc |
|
- | rw-r--r-- | 934 | thm_rule_win.doc |
|
- | rw-r--r-- | 630 | transform.doc |
|
- | rw-r--r-- | 784 | transform_win.doc |
|
- | rw-r--r-- | 276 | traverse.doc |
|
- | rw-r--r-- | 585 | used_conjectures.doc |
|
- | rw-r--r-- | 541 | used_hypotheses.doc |
|
- | rw-r--r-- | 436 | win_thm.doc |
|
- | rw-r--r-- | 254 | window_version.doc |