package info
(click to toggle)
hol88 2.02.19940316-33
- links: PTS
- area: main
- in suites: stretch
- size: 65,988 kB
- ctags: 21,623
- sloc: ml: 199,939; ansic: 9,666; sh: 7,118; makefile: 6,095; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
Folder: entries
 |
.. (parent) | |||
 |
- | rw-r--r-- | 25 | .exrc |
|
- | rw-r--r-- | 709 | AND_PEXISTS_CONV.doc |
|
- | rw-r--r-- | 530 | AND_PFORALL_CONV.doc |
|
- | rw-r--r-- | 439 | CURRY_CONV.doc |
|
- | rw-r--r-- | 688 | CURRY_EXISTS_CONV.doc |
|
- | rw-r--r-- | 682 | CURRY_FORALL_CONV.doc |
|
- | rw-r--r-- | 929 | FILTER_PGEN_TAC.doc |
|
- | rw-r--r-- | 2,644 | FILTER_PSTRIP_TAC.doc |
|
- | rw-r--r-- | 1,522 | FILTER_PSTRIP_THEN.doc |
|
- | rw-r--r-- | 1,075 | GEN_PALPHA_CONV.doc |
|
- | rw-r--r-- | 836 | GPSPEC.doc |
|
- | rw-r--r-- | 752 | HALF_MK_PABS.doc |
|
- | rw-r--r-- | 753 | IPSPEC.doc |
|
- | rw-r--r-- | 706 | IPSPECL.doc |
|
- | rw-r--r-- | 699 | LEFT_AND_PEXISTS_CONV.doc |
|
- | rw-r--r-- | 648 | LEFT_AND_PFORALL_CONV.doc |
|
- | rw-r--r-- | 697 | LEFT_IMP_PEXISTS_CONV.doc |
|
- | rw-r--r-- | 693 | LEFT_IMP_PFORALL_CONV.doc |
|
- | rw-r--r-- | 803 | LEFT_LIST_PBETA.doc |
|
- | rw-r--r-- | 695 | LEFT_OR_PEXISTS_CONV.doc |
|
- | rw-r--r-- | 701 | LEFT_OR_PFORALL_CONV.doc |
|
- | rw-r--r-- | 692 | LEFT_PBETA.doc |
|
- | rw-r--r-- | 929 | LIST_MK_PEXISTS.doc |
|
- | rw-r--r-- | 923 | LIST_MK_PFORALL.doc |
|
- | rw-r--r-- | 937 | LIST_PBETA_CONV.doc |
|
- | rw-r--r-- | 569 | MK_PABS.doc |
|
- | rw-r--r-- | 491 | MK_PAIR.doc |
|
- | rw-r--r-- | 598 | MK_PEXISTS.doc |
|
- | rw-r--r-- | 590 | MK_PFORALL.doc |
|
- | rw-r--r-- | 583 | MK_PSELECT.doc |
|
- | rw-r--r-- | 504 | NOT_PEXISTS_CONV.doc |
|
- | rw-r--r-- | 576 | NOT_PFORALL_CONV.doc |
|
- | rw-r--r-- | 551 | OR_PEXISTS_CONV.doc |
|
- | rw-r--r-- | 730 | OR_PFORALL_CONV.doc |
|
- | rw-r--r-- | 582 | PABS.doc |
|
- | rw-r--r-- | 967 | PABS_CONV.doc |
|
- | rw-r--r-- | 681 | PAIR_CONV.doc |
|
- | rw-r--r-- | 1,587 | PALPHA.doc |
|
- | rw-r--r-- | 1,793 | PALPHA_CONV.doc |
|
- | rw-r--r-- | 796 | PART_PMATCH.doc |
|
- | rw-r--r-- | 1,629 | PBETA_CONV.doc |
|
- | rw-r--r-- | 653 | PBETA_RULE.doc |
|
- | rw-r--r-- | 632 | PBETA_TAC.doc |
|
- | rw-r--r-- | 927 | PCHOOSE.doc |
|
- | rw-r--r-- | 748 | PCHOOSE_TAC.doc |
|
- | rw-r--r-- | 942 | PCHOOSE_THEN.doc |
|
- | rw-r--r-- | 394 | PETA_CONV.doc |
|
- | rw-r--r-- | 583 | PEXISTENCE.doc |
|
- | rw-r--r-- | 1,167 | PEXISTS.doc |
|
- | rw-r--r-- | 1,140 | PEXISTS_AND_CONV.doc |
|
- | rw-r--r-- | 649 | PEXISTS_CONV.doc |
|
- | rw-r--r-- | 936 | PEXISTS_EQ.doc |
|
- | rw-r--r-- | 799 | PEXISTS_IMP.doc |
|
- | rw-r--r-- | 1,134 | PEXISTS_IMP_CONV.doc |
|
- | rw-r--r-- | 502 | PEXISTS_NOT_CONV.doc |
|
- | rw-r--r-- | 534 | PEXISTS_OR_CONV.doc |
|
- | rw-r--r-- | 658 | PEXISTS_RULE.doc |
|
- | rw-r--r-- | 725 | PEXISTS_TAC.doc |
|
- | rw-r--r-- | 1,106 | PEXISTS_UNIQUE_CONV.doc |
|
- | rw-r--r-- | 753 | PEXT.doc |
|
- | rw-r--r-- | 537 | PFORALL_AND_CONV.doc |
|
- | rw-r--r-- | 898 | PFORALL_EQ.doc |
|
- | rw-r--r-- | 1,132 | PFORALL_IMP_CONV.doc |
|
- | rw-r--r-- | 498 | PFORALL_NOT_CONV.doc |
|
- | rw-r--r-- | 1,127 | PFORALL_OR_CONV.doc |
|
- | rw-r--r-- | 753 | PGEN.doc |
|
- | rw-r--r-- | 808 | PGENL.doc |
|
- | rw-r--r-- | 734 | PGEN_TAC.doc |
|
- | rw-r--r-- | 1,365 | PMATCH_MP.doc |
|
- | rw-r--r-- | 1,195 | PMATCH_MP_TAC.doc |
|
- | rw-r--r-- | 693 | PSELECT_CONV.doc |
|
- | rw-r--r-- | 1,261 | PSELECT_ELIM.doc |
|
- | rw-r--r-- | 799 | PSELECT_EQ.doc |
|
- | rw-r--r-- | 756 | PSELECT_INTRO.doc |
|
- | rw-r--r-- | 719 | PSELECT_RULE.doc |
|
- | rw-r--r-- | 917 | PSKOLEM_CONV.doc |
|
- | rw-r--r-- | 1,010 | PSPEC.doc |
|
- | rw-r--r-- | 949 | PSPECL.doc |
|
- | rw-r--r-- | 775 | PSPEC_ALL.doc |
|
- | rw-r--r-- | 777 | PSPEC_PAIR.doc |
|
- | rw-r--r-- | 899 | PSPEC_TAC.doc |
|
- | rw-r--r-- | 1,922 | PSTRIP_ASSUME_TAC.doc |
|
- | rw-r--r-- | 1,782 | PSTRIP_GOAL_THEN.doc |
|
- | rw-r--r-- | 1,841 | PSTRIP_TAC.doc |
|
- | rw-r--r-- | 2,359 | PSTRIP_THM_THEN.doc |
|
- | rw-r--r-- | 1,299 | PSTRUCT_CASES_TAC.doc |
|
- | rw-r--r-- | 1,603 | PSUB_CONV.doc |
|
- | rw-r--r-- | 1,025 | P_FUN_EQ_CONV.doc |
|
- | rw-r--r-- | 1,091 | P_PCHOOSE_TAC.doc |
|
- | rw-r--r-- | 1,413 | P_PCHOOSE_THEN.doc |
|
- | rw-r--r-- | 781 | P_PGEN_TAC.doc |
|
- | rw-r--r-- | 1,067 | P_PSKOLEM_CONV.doc |
|
- | rw-r--r-- | 707 | RIGHT_AND_PEXISTS_CONV.doc |
|
- | rw-r--r-- | 704 | RIGHT_AND_PFORALL_CONV.doc |
|
- | rw-r--r-- | 688 | RIGHT_IMP_PEXISTS_CONV.doc |
|
- | rw-r--r-- | 697 | RIGHT_IMP_PFORALL_CONV.doc |
|
- | rw-r--r-- | 809 | RIGHT_LIST_PBETA.doc |
|
- | rw-r--r-- | 701 | RIGHT_OR_PEXISTS_CONV.doc |
|
- | rw-r--r-- | 707 | RIGHT_OR_PFORALL_CONV.doc |
|
- | rw-r--r-- | 699 | RIGHT_PBETA.doc |
|
- | rw-r--r-- | 495 | SWAP_PEXISTS_CONV.doc |
|
- | rw-r--r-- | 475 | SWAP_PFORALL_CONV.doc |
|
- | rw-r--r-- | 351 | UNCURRY_CONV.doc |
|
- | rw-r--r-- | 688 | UNCURRY_EXISTS_CONV.doc |
|
- | rw-r--r-- | 682 | UNCURRY_FORALL_CONV.doc |
|
- | rw-r--r-- | 501 | UNPBETA_CONV.doc |
|
- | rw-r--r-- | 273 | bndpair.doc |
|
- | rw-r--r-- | 395 | dest_pabs.doc |
|
- | rw-r--r-- | 489 | dest_pexists.doc |
|
- | rw-r--r-- | 483 | dest_pforall.doc |
|
- | rw-r--r-- | 353 | dest_prod.doc |
|
- | rw-r--r-- | 437 | dest_pselect.doc |
|
- | rw-r--r-- | 1,024 | genlike.doc |
|
- | rw-r--r-- | 305 | is_pabs.doc |
|
- | rw-r--r-- | 353 | is_pexists.doc |
|
- | rw-r--r-- | 351 | is_pforall.doc |
|
- | rw-r--r-- | 226 | is_prod.doc |
|
- | rw-r--r-- | 322 | is_pselect.doc |
|
- | rw-r--r-- | 364 | is_pvar.doc |
|
- | rw-r--r-- | 426 | list_mk_pabs.doc |
|
- | rw-r--r-- | 596 | list_mk_pexists.doc |
|
- | rw-r--r-- | 595 | list_mk_pforall.doc |
|
- | rw-r--r-- | 329 | mk_pabs.doc |
|
- | rw-r--r-- | 389 | mk_pexists.doc |
|
- | rw-r--r-- | 390 | mk_pforall.doc |
|
- | rw-r--r-- | 252 | mk_prod.doc |
|
- | rw-r--r-- | 357 | mk_pselect.doc |
|
- | rw-r--r-- | 456 | occs_in.doc |
|
- | rw-r--r-- | 377 | paconv.doc |
|
- | rw-r--r-- | 258 | pbody.doc |
|
- | rw-r--r-- | 1,488 | pvariant.doc |
|
- | rw-r--r-- | 419 | rip_pair.doc |
|
- | rw-r--r-- | 420 | strip_pabs.doc |
|
- | rw-r--r-- | 476 | strip_pexists.doc |
|
- | rw-r--r-- | 471 | strip_pforall.doc |