diff options
author | Hendrik Tews <hendrik@askra.de> | 2016-10-26 09:58:52 +0200 |
---|---|---|
committer | Hendrik Tews <hendrik@askra.de> | 2016-10-27 09:26:40 +0200 |
commit | cda28bfda3154c9040ec11abea1021755992e36a (patch) | |
tree | 1302882de7efdf6c004082e21122d2652439d10e | |
parent | 24858fa6989ae8b41e0c31fca5499cceeb4f21e8 (diff) |
delete TAGS file from repository
-rw-r--r-- | TAGS | 3081 |
1 files changed, 0 insertions, 3081 deletions
@@ -1,3081 +0,0 @@ - -ccc/ccc.el,87 -(defvar ccc-keywords 17,587 -(defvar ccc-tactics 18,613 -(defvar ccc-tacticals 19,638 - -coq/coq-abbrev.el,590 -(defun holes-show-doc 12,313 -(defun coq-local-vars-list-show-doc 16,390 -(defconst coq-tactics-menu21,490 -(defconst coq-tactics-abbrev-table26,746 -(defconst coq-tacticals-menu29,863 -(defconst coq-tacticals-abbrev-table33,972 -(defconst coq-commands-menu36,1063 -(defconst coq-commands-abbrev-table43,1286 -(defconst coq-terms-menu46,1375 -(defconst coq-terms-abbrev-table51,1513 -(defun coq-install-abbrevs 58,1707 -(defconst coq-menu-common-entries81,2663 -(defpgdefault menu-entries182,7261 -(defpgdefault help-menu-entries216,8368 -(defpgdefault other-buffers-menu-entries 220,8498 - -coq/coq-compile-common.el,2047 -(defun get-coq-library-directory 31,821 -(defconst coq-library-directory 37,1008 -(defcustom coq-dependency-analyzer40,1135 -(defcustom coq-compiler46,1275 -(defun coq-par-enable 60,1800 -(defun coq-par-disable 70,2161 -(defun coq-seq-enable 80,2541 -(defun coq-seq-disable 86,2747 -(defun coq-load-path-safep 95,2998 -(defun coq-switch-compilation-method 115,3594 -(defun number-of-cpus 124,3829 -(defvar coq-internal-max-jobs 138,4170 -(defun coq-max-jobs-setter 141,4279 -(defgroup coq-auto-compile 157,4741 -(defpacustom compile-before-require 162,4892 -(defpacustom compile-parallel-in-background 174,5384 -(defcustom coq-max-background-compilation-jobs 195,6275 -(defcustom coq-compile-command 209,6964 -(defconst coq-compile-substitution-list239,8243 -(defcustom coq-load-path 259,9164 -(defcustom coq-compile-auto-save 296,10909 -(defcustom coq-lock-ancestors 321,11966 -(defpacustom confirm-external-compilation 330,12287 -(defcustom coq-load-path-include-current 339,12594 -(defcustom coq-compile-ignored-directories 348,12912 -(defcustom coq-compile-ignore-library-directory 361,13544 -(defcustom coq-coqdep-error-regexp373,14032 -(defconst coq-require-command-regexp390,14811 -(defconst coq-require-id-regexp397,15168 -(defvar coq-compile-history 405,15602 -(defvar coq-compile-response-buffer 408,15686 -(defvar coq-debug-auto-compilation 412,15821 -(defun time-less-or-equal 418,15930 -(defun coq-max-dep-mod-time 426,16268 -(defun coq-option-of-load-path-entry 449,17073 -(defun coq-include-options 463,17588 -(defun coq-prog-args 487,18607 -(defun coq-compile-ignore-file 496,18880 -(defun coq-library-src-of-obj-file 522,19802 -(defun coq-unlock-ancestor 531,20126 -(defun coq-unlock-all-ancestors-of-span 538,20421 -(defun coq-init-compile-response-buffer 546,20706 -(defun coq-display-compile-response-buffer 569,21778 -(defvar coq-compile-buffer-with-current-require582,22297 -(defun coq-compile-save-buffer-filter 588,22533 -(defun coq-compile-save-some-buffers 599,22959 -(defun coq-switch-buffer-kill-proof-shell 624,23913 - -coq/coq-db.el,678 -(defconst coq-syntax-db 24,596 -(defun coq-insert-from-db 70,2319 -(defun coq-build-regexp-list-from-db 88,3050 -(defun coq-build-opt-regexp-from-db 107,3856 -(defun max-length-db 126,4677 -(defun coq-build-menu-from-db-internal 138,4952 -(defun coq-build-title-menu 175,6493 -(defun coq-sort-menu-entries 184,6861 -(defun coq-build-menu-from-db 190,6991 -(defcustom coq-holes-minor-mode 212,7830 -(defun coq-build-abbrev-table-from-db 218,7974 -(defun filter-state-preserving 237,8600 -(defun filter-state-changing 242,8754 -(defface coq-solve-tactics-face249,8975 -(defface coq-cheat-face258,9266 -(defconst coq-solve-tactics-face 266,9515 -(defconst coq-cheat-face 270,9679 - -coq/coq.el,9459 -(defcustom coq-prog-name63,2161 -(defcustom coq-translate-to-v8 82,3012 -(defun coq-build-prog-args 87,3127 -(defcustom coq-use-makefile 97,3450 -(defcustom coq-default-undo-limit 103,3622 -(defconst coq-shell-init-cmd108,3750 -(defcustom coq-prog-env 117,4077 -(defconst coq-shell-restart-cmd 125,4326 -(defvar coq-shell-prompt-pattern127,4380 -(defvar coq-shell-cd 135,4683 -(defvar coq-shell-proof-completed-regexp 139,4843 -(defvar coq-goal-regexp142,5058 -(defcustom coq-tags 146,5149 -(defconst coq-interrupt-regexp 151,5297 -(defcustom coq-www-home-page 154,5390 -(defcustom coq-end-goals-regexp-show-subgoals 159,5497 -(defcustom coq-end-goals-regexp-hide-subgoals166,5781 -(defgroup coq-proof-tree 177,6113 -(defcustom coq-proof-tree-ignored-commands-regexp185,6476 -(defcustom coq-navigation-command-regexp194,6870 -(defcustom coq-proof-tree-cheating-regexp201,7124 -(defcustom coq-proof-tree-new-layer-command-regexp207,7264 -(defcustom coq-proof-tree-current-goal-regexp213,7470 -(defcustom coq-proof-tree-update-goal-regexp221,7806 -(defcustom coq-proof-tree-additional-subgoal-ID-regexp228,8040 -(defcustom coq-proof-tree-existential-regexp 234,8238 -(defcustom coq-proof-tree-instantiated-existential-regexp239,8392 -(defcustom coq-proof-tree-existentials-state-start-regexp245,8612 -(defcustom coq-proof-tree-existentials-state-end-regexp 251,8802 -(defcustom coq-proof-tree-branch-finished-regexp256,8971 -(defvar coq-outline-regexp272,9472 -(defvar coq-outline-heading-end-regexp 281,9746 -(defvar coq-shell-outline-regexp 283,9800 -(defvar coq-shell-outline-heading-end-regexp 284,9850 -(defconst coq-state-preserving-tactics-regexp287,9914 -(defconst coq-state-changing-commands-regexp289,10016 -(defconst coq-state-preserving-commands-regexp291,10125 -(defconst coq-commands-regexp293,10238 -(defvar coq-retractable-instruct-regexp295,10317 -(defvar coq-non-retractable-instruct-regexp297,10409 -(defcustom coq-use-smie 329,11105 -(defconst coq-script-command-end-regexp 354,11943 -(defun coq-script-parse-function 363,12372 -(defun coq-set-undo-limit 370,12598 -(defun build-list-id-from-string 376,12730 -(defun coq-last-prompt-info 385,13205 -(defun coq-last-prompt-info-safe 403,14099 -(defvar coq-last-but-one-statenum 411,14452 -(defvar coq-last-but-one-proofnum 418,14749 -(defvar coq-last-but-one-proofstack 421,14847 -(defsubst coq-get-span-statenum 424,14957 -(defsubst coq-get-span-proofnum 428,15072 -(defsubst coq-get-span-proofstack 432,15187 -(defsubst coq-set-span-statenum 436,15331 -(defsubst coq-get-span-goalcmd 440,15462 -(defsubst coq-set-span-goalcmd 444,15576 -(defsubst coq-set-span-proofnum 448,15706 -(defsubst coq-set-span-proofstack 452,15837 -(defsubst proof-last-locked-span 456,15997 -(defun proof-clone-buffer 460,16131 -(defun proof-store-buffer-win 474,16668 -(defun proof-store-response-win 485,17161 -(defun proof-store-goals-win 489,17288 -(defun coq-set-state-infos 501,17820 -(defun count-not-intersection 539,19910 -(defun coq-find-and-forget 569,21162 -(defvar coq-current-goal 596,22467 -(defun coq-goal-hyp 599,22532 -(defun coq-state-preserving-p 612,23012 -(defun coq-hide-additional-subgoals-switch 622,23306 -(defconst notation-print-kinds-table634,23647 -(defun coq-PrintScope 638,23814 -(defun coq-remove-trailing-dot 656,24363 -(defun coq-id-at-point 664,24600 -(defun coq-guess-or-ask-for-string 678,25163 -(defun coq-ask-do 697,25778 -(defun coq-flag-is-on-p 706,26161 -(defun coq-command-with-set-unset 712,26368 -(defun coq-ask-do-set-unset 723,27018 -(defun coq-ask-do-show-implicits 733,27548 -(defun coq-ask-do-show-all 741,27908 -(defsubst coq-put-into-brackets 762,28589 -(defsubst coq-put-into-quotes 765,28650 -(defun coq-SearchIsos 768,28709 -(defun coq-SearchConstant 776,28948 -(defun coq-Searchregexp 780,29041 -(defun coq-SearchRewrite 786,29182 -(defun coq-SearchAbout 790,29279 -(defun coq-Print 796,29422 -(defun coq-Print-with-implicits 804,29692 -(defun coq-Print-with-all 809,29846 -(defun coq-About 814,29988 -(defun coq-About-with-implicits 821,30195 -(defun coq-About-with-all 826,30344 -(defun coq-LocateConstant 832,30482 -(defun coq-LocateLibrary 837,30585 -(defun coq-LocateNotation 842,30702 -(defun coq-Pwd 850,30933 -(defun coq-Inspect 855,31057 -(defun coq-PrintSection(859,31157 -(defun coq-Print-implicit 863,31250 -(defun coq-Check 868,31401 -(defun coq-Check-show-implicits 876,31655 -(defun coq-Check-show-all 881,31793 -(defun coq-get-response-string-at 886,31919 -(defun coq-Show 900,32509 -(defun coq-Show-with-implicits 930,33917 -(defun coq-Show-with-all 935,34073 -(defun coq-Compile 962,35450 -(defun coq-guess-command-line 974,35775 -(defpacustom use-project-file 1012,37560 -(defpacustom project-filename 1022,38036 -(defun coq-find-project-file 1039,38775 -(defconst coq-load-path--R-regexp1055,39627 -(defconst coq-load-path--I-regexp1058,39746 -(defconst coq-prog-args-regexp1063,39952 -(defun coq-read-option-from-project-file 1066,40062 -(defun coq-search-load-path 1091,41273 -(defun coq-search-prog-args 1101,41705 -(defun coq-load-project-file 1108,41911 -(defun coq-local-variables-if-enabled 1134,43305 -(defun coq-mode-config 1171,44627 -(defun coq-shell-mode-config 1284,48815 -(defun coq-goals-mode-config 1377,52762 -(defun coq-response-config 1384,53006 -(defpacustom hide-additional-subgoals 1407,53723 -(defpacustom printing-depth 1428,54390 -(defpacustom undo-depth 1433,54551 -(defpacustom time-commands 1438,54717 -(defun coq-proof-tree-get-proof-info 1448,54922 -(defun coq-extract-instantiated-existentials 1458,55310 -(defun coq-show-sequent-command 1467,55702 -(defun coq-proof-tree-get-new-subgoals 1471,55856 -(defun coq-find-begin-of-unfinished-proof 1515,57981 -(defun coq-proof-tree-find-undo-position 1533,58815 -(defun coq-preprocessing 1553,59556 -(defun coq-fake-constant-markup 1567,60011 -(defun coq-create-span-menu 1583,60616 -(defconst module-kinds-table1601,61129 -(defconst modtype-kinds-table1605,61278 -(defun coq-postfix-.v-p 1609,61407 -(defun coq-directories-files 1612,61468 -(defun coq-remove-dot-v-extension 1618,61696 -(defun coq-load-path-to-paths 1621,61757 -(defun coq-build-accessible-modules-list 1624,61836 -(defun coq-insert-section-or-module 1631,62153 -(defconst reqkinds-kinds-table1653,63033 -(defun coq-insert-requires 1657,63190 -(defun coq-end-Section 1672,63770 -(defun coq-insert-intros 1690,64348 -(defvar coq-commands-accepting-as 1703,64880 -(defvar coq-last-input-action 1705,64979 -(defun coq-insert-infoH 1711,65195 -(defun coq-auto-insert-as 1725,65860 -(defpacustom auto-insert-as 1735,66274 -(defun coq-tactic-already-has-an-as-close(1742,66509 -(defun coq-insert-as 1757,67274 -(defun coq-insert-as-in-region 1797,69418 -(defun coq-insert-match 1808,69699 -(defun coq-insert-solve-tactic 1837,70868 -(defun coq-insert-tactic 1843,71119 -(defun coq-insert-tactical 1849,71321 -(defun coq-insert-command 1855,71552 -(defun coq-insert-term 1860,71717 -(define-key coq-keymap 1866,71900 -(define-key coq-keymap 1867,71958 -(define-key coq-keymap 1868,72015 -(define-key coq-keymap 1869,72084 -(define-key coq-keymap 1870,72140 -(define-key coq-keymap 1871,72198 -(define-key coq-keymap 1872,72248 -(define-key coq-keymap 1873,72321 -(define-key coq-keymap 1874,72378 -(define-key coq-keymap 1875,72441 -(define-key coq-keymap 1878,72519 -(define-key coq-keymap 1879,72568 -(define-key coq-keymap 1880,72623 -(define-key coq-keymap 1881,72675 -(define-key coq-keymap 1882,72730 -(define-key coq-keymap 1883,72780 -(define-key coq-keymap 1884,72830 -(define-key coq-keymap 1885,72886 -(define-key coq-keymap 1886,72936 -(define-key coq-keymap 1887,72980 -(define-key coq-keymap 1888,73039 -(define-key coq-goals-mode-map 1896,73307 -(define-key coq-goals-mode-map 1897,73389 -(define-key coq-goals-mode-map 1898,73471 -(define-key coq-goals-mode-map 1899,73558 -(define-key coq-goals-mode-map 1900,73640 -(define-key coq-goals-mode-map 1901,73728 -(define-key coq-goals-mode-map 1902,73809 -(define-key coq-goals-mode-map 1903,73896 -(define-key coq-goals-mode-map 1904,73980 -(define-key coq-response-mode-map 1907,74058 -(define-key coq-response-mode-map 1908,74143 -(define-key coq-response-mode-map 1909,74228 -(define-key coq-response-mode-map 1910,74318 -(define-key coq-response-mode-map 1911,74403 -(define-key coq-response-mode-map 1912,74494 -(define-key coq-response-mode-map 1913,74578 -(define-key coq-response-mode-map 1914,74678 -(define-key coq-response-mode-map 1915,74775 -(defvar last-coq-error-location 1922,74925 -(defun coq-get-last-error-location 1930,75309 -(defun coq-highlight-error 1980,77872 -(defun coq-highlight-error-hook 2008,78953 -(defun coq-first-word-before 2018,79170 -(defun coq-get-from-to-paren 2028,79501 -(defun coq-show-first-goal 2041,79907 -(defvar coq-modeline-string2 2057,80572 -(defvar coq-modeline-string1 2058,80606 -(defvar coq-modeline-string0 2059,80640 -(defun coq-build-subgoals-string 2060,80681 -(defun coq-update-minor-mode-alist 2066,80865 -(defun is-not-split-vertic 2100,82434 -(defun coq-optimise-resp-windows 2114,83227 -(defcustom coq-double-hit-enable 2154,85054 -(defadvice proof-electric-terminator-enable 2173,85840 -(defvar coq-double-hit-delay 2181,86218 -(defvar coq-double-hit-timer 2184,86333 -(defvar coq-double-hit-hot 2187,86413 -(defun coq-unset-double-hit-hot 2191,86509 -(defun coq-colon-self-insert 2199,86840 -(defun coq-terminator-insert 2213,87396 -(defun coq-activate-ml4pg 2230,88187 - -coq/coq-indent.el,2698 -(defconst coq-any-command-regexp20,368 -(defconst coq-indent-inner-regexp23,442 -(defconst coq-comment-start-regexp 33,799 -(defconst coq-comment-end-regexp 34,842 -(defconst coq-comment-start-or-end-regexp35,883 -(defconst coq-indent-open-regexp37,991 -(defconst coq-indent-close-regexp42,1188 -(defconst coq-indent-closepar-regexp 48,1387 -(defconst coq-indent-closematch-regexp 49,1432 -(defconst coq-indent-openpar-regexp 50,1503 -(defconst coq-indent-openmatch-regexp 51,1547 -(defconst coq-tacticals-tactics-regex52,1627 -(defconst coq-indent-any-regexp54,1746 -(defconst coq-indent-kw58,1962 -(defconst coq-indent-pattern-regexp 68,2428 -(defun coq-indent-goal-command-p 72,2531 -(defconst coq-period-end-command93,3549 -(defconst coq-curlybracket-end-command99,3831 -(defconst coq-bullet-end-command104,4060 -(defconst coq-end-command-regexp117,4515 -(defun coq-search-comment-delimiter-forward 133,5240 -(defun coq-search-comment-delimiter-backward 142,5570 -(defun coq-skip-until-one-comment-backward 149,5844 -(defun coq-skip-until-one-comment-forward 164,6551 -(defun coq-looking-at-comment 175,7069 -(defun coq-find-comment-start 180,7234 -(defun coq-find-comment-end 192,7711 -(defun coq-looking-at-syntactic-context 204,8204 -(defconst coq-end-command-or-comment-regexp210,8426 -(defconst coq-end-command-or-comment-start-regexp213,8535 -(defun coq-find-not-in-comment-backward 216,8652 -(defun coq-find-not-in-comment-forward 235,9531 -(defun coq-is-on-ending-context 261,10723 -(defun coq-empty-command-p 270,10936 -(defun coq-script-parse-cmdend-forward 285,11677 -(defun coq-script-parse-cmdend-backward 337,14178 -(defun coq-find-current-start 378,16099 -(defun coq-find-real-start 387,16425 -(defun same-line 393,16643 -(defun coq-command-at-point 396,16730 -(defun coq-commands-at-line 411,17341 -(defun coq-indent-only-spaces-on-line 435,18307 -(defun coq-indent-find-reg 441,18584 -(defun coq-find-no-syntactic-on-line 455,19120 -(defun coq-back-to-indentation-prevline 468,19593 -(defun coq-find-unclosed 514,21660 -(defun coq-find-at-same-level-zero 544,22970 -(defun coq-find-unopened 573,24236 -(defun coq-find-last-unopened 616,25670 -(defun coq-end-offset 627,26067 -(defun coq-add-iter 652,26837 -(defun coq-goal-count 655,26943 -(defun coq-save-count 657,27015 -(defun coq-proof-count 662,27214 -(defun coq-goal-save-diff-maybe-proof 668,27500 -(defun coq-indent-command-offset 678,27794 -(defun coq-indent-expr-offset 744,30975 -(defun coq-indent-comment-offset 863,35857 -(defun coq-indent-offset 895,37309 -(defun coq-indent-calculate 914,38183 -(defun coq-indent-line 917,38271 -(defun coq-indent-line-not-comments 927,38637 -(defun coq-indent-region 937,39026 - -coq/coq-local-vars.el,229 -(defconst coq-local-vars-doc 23,470 -(defun coq-insert-coq-prog-name 86,2815 -(defun coq-read-directory 99,3383 -(defun coq-ask-load-path 116,4198 -(defun coq-ask-prog-name 135,5165 -(defun coq-ask-insert-coq-prog-name 152,5876 - -coq/coq-par-compile.el,2176 -(defvar coq-par-ancestor-files 251,10947 -(defvar coq-current-background-jobs 267,11596 -(defvar coq-compilation-object-hash 270,11685 -(defvar coq-last-compilation-job 278,12058 -(defvar coq-par-next-id 282,12201 -(defun split-list-at-predicate 289,12358 -(defun coq-par-time-less 313,13210 -(defun coq-par-init-compilation-hash 323,13558 -(defun coq-par-init-ancestor-hash 327,13719 -(defun coq-par-new-compilation-queue 338,14004 -(defvar coq-par-compilation-queue 342,14126 -(defun coq-par-enqueue 346,14310 -(defun coq-par-dequeue 352,14544 -(defun coq-par-find-dependency-circle-for-job 411,16514 -(defun coq-par-find-dependency-circle 434,17285 -(defun coq-par-coq-arguments 455,18019 -(defun coq-par-analyse-coq-dep-exit 463,18388 -(defun coq-par-get-library-dependencies 482,19171 -(defun coq-par-map-module-id-to-obj-file 526,21141 -(defun coq-par-kill-all-processes 585,23970 -(defun coq-par-unlock-ancestors-on-error 612,24984 -(defun coq-par-emergency-cleanup 622,25327 -(defun coq-par-process-filter 637,25888 -(defun coq-par-start-process 642,26097 -(defun coq-par-process-sentinel 676,27711 -(defun coq-par-job-coqc-finished 728,29684 -(defun coq-par-job-is-ready 733,29853 -(defun coq-par-dependencies-ready 737,29959 -(defun coq-par-add-coqc-dependency 741,30103 -(defun coq-par-add-queue-dependency 750,30516 -(defun coq-par-get-obj-mod-time 760,30982 -(defun coq-par-job-needs-compilation 774,31512 -(defun coq-par-kickoff-queue-maybe 803,32743 -(defun coq-par-compile-job-maybe 869,35612 -(defun coq-par-decrease-coqc-dependency 883,36281 -(defun coq-par-kickoff-coqc-dependants 918,38051 -(defun coq-par-start-coqdep 966,40249 -(defun coq-par-start-task 983,40936 -(defun coq-par-start-jobs-until-full 999,41497 -(defun coq-par-start-or-enqueue 1008,41794 -(defun coq-par-create-library-job 1017,42181 -(defun coq-par-process-coqdep-result 1093,45567 -(defun coq-par-coqc-continuation 1151,48050 -(defun coq-par-handle-module 1174,48896 -(defun coq-par-handle-require-list 1203,50120 -(defun coq-par-item-require-predicate 1250,52245 -(defun coq-par-preprocess-require-commands-internal 1259,52568 -(defun coq-par-preprocess-require-commands 1326,55407 - -coq/coq-seq-compile.el,422 -(defun coq-seq-lock-ancestor 38,1174 -(defun coq-seq-get-library-dependencies 56,2005 -(defun coq-seq-compile-library 109,4420 -(defun coq-seq-compile-library-if-necessary 136,5649 -(defun coq-seq-make-lib-up-to-date 182,7533 -(defun coq-seq-auto-compile-externally 240,10027 -(defun coq-seq-map-module-id-to-obj-file 284,12191 -(defun coq-seq-check-module 337,14809 -(defun coq-seq-preprocess-require-commands 365,16275 - -coq/coq-smie-lexer.el,859 -(defun coq-dot-friend-p 25,1267 -(defun coq-time-indent 30,1437 -(defun coq-time-indent-region 36,1578 -(defun coq-smie-is-tactic 45,1749 -(defun coq-smie-.-deambiguate 55,1982 -(defun coq-smie-complete-qualid-backward 88,2927 -(defun coq-smie-find-unclosed-match-backward 96,3147 -(defun coq-smie-with-deambiguate(106,3475 -(defun coq-smie-search-token-forward 123,4057 -(defun coq-smie-search-token-backward 168,5949 -(defun coq-lonely-:=212,7802 -(defun coq-smie-detect-goal-command 229,8570 -(defun coq-smie-module-deambiguate 245,9340 -(defconst coq-smie-proof-end-tokens264,10236 -(defun coq-smie-forward-token 268,10387 -(defun coq-is-at-command-real-start(343,13317 -(defun coq-smie-:=348,13417 -(defun coq-smie-backward-token 374,14416 -(defcustom coq-indent-box-style 565,20577 -(defconst coq-smie-grammar588,21319 -(defun coq-smie-rules 720,26572 - -coq/coq-syntax.el,2786 -(defcustom coq-user-tactics-db 21,586 -(defcustom coq-user-commands-db 38,1099 -(defcustom coq-user-tacticals-db 54,1618 -(defcustom coq-user-solve-tactics-db 70,2139 -(defcustom coq-user-cheat-tactics-db 86,2658 -(defcustom coq-user-reserved-db 105,3204 -(defvar coq-tactics-db123,3735 -(defvar coq-solve-tactics-db296,12869 -(defvar coq-solve-cheat-tactics-db323,13892 -(defvar develock-coq-font-lock-keywords331,14098 -(defvar coq-tacticals-db342,14405 -(defvar coq-decl-db366,15291 -(defvar coq-defn-db391,16747 -(defvar coq-goal-starters-db456,21469 -(defvar coq-other-commands-db487,23350 -(defvar coq-commands-db622,33335 -(defvar coq-terms-db629,33555 -(defun coq-count-match 691,36170 -(defun coq-module-opening-p 707,36899 -(defun coq-section-command-p 717,37333 -(defun coq-goal-command-str-p 721,37430 -(defun coq-goal-command-p 747,38755 -(defvar coq-keywords-save-strict756,39099 -(defvar coq-keywords-save763,39340 -(defun coq-save-command-p 768,39419 -(defvar coq-keywords-kill-goal779,39747 -(defvar coq-keywords-state-changing-misc-commands783,39837 -(defvar coq-keywords-goal786,39962 -(defvar coq-keywords-decl789,40045 -(defvar coq-keywords-defn792,40119 -(defvar coq-keywords-state-changing-commands796,40194 -(defvar coq-keywords-state-preserving-commands805,40454 -(defvar coq-keywords-commands810,40670 -(defvar coq-solve-tactics815,40818 -(defvar coq-solve-tactics-regexp819,40939 -(defvar coq-solve-cheat-tactics823,41073 -(defvar coq-solve-cheat-tactics-regexp827,41218 -(defvar coq-tacticals831,41376 -(defvar coq-reserved837,41515 -(defvar coq-reserved-regexp 847,41850 -(defvar coq-state-changing-tactics851,41961 -(defvar coq-state-preserving-tactics854,42070 -(defvar coq-tactics858,42184 -(defvar coq-tactics-regexp 861,42273 -(defvar coq-retractable-instruct864,42428 -(defvar coq-non-retractable-instruct867,42538 -(defvar coq-keywords871,42666 -(defun proof-regexp-alt-list-symb 877,42890 -(defvar coq-keywords-regexp 880,42995 -(defvar coq-symbols883,43068 -(defvar coq-error-regexp 905,43309 -(defvar coq-id 908,43537 -(defvar coq-id-shy 909,43562 -(defvar coq-ids 912,43655 -(defun coq-first-abstr-regexp 914,43721 -(defcustom coq-variable-highlight-enable 917,43816 -(defvar coq-font-lock-terms923,43943 -(defconst coq-save-command-regexp-strict945,45026 -(defconst coq-save-command-regexp951,45194 -(defconst coq-save-with-hole-regexp956,45347 -(defconst coq-goal-command-regexp960,45507 -(defconst coq-goal-with-hole-regexp963,45609 -(defconst coq-decl-with-hole-regexp967,45743 -(defconst coq-defn-with-hole-regexp974,45993 -(defconst coq-with-with-hole-regexp984,46283 -(defvar coq-font-lock-keywords-1999,46813 -(defvar coq-font-lock-keywords 1027,48148 -(defun coq-init-syntax-table 1029,48206 -(defconst coq-generic-expression1054,48933 - -coq/coq-unicode-tokens.el,454 -(defconst coq-token-format 39,1427 -(defconst coq-token-match 40,1475 -(defconst coq-hexcode-match 41,1506 -(defun coq-unicode-tokens-set 43,1540 -(defcustom coq-token-symbol-map49,1768 -(defcustom coq-shortcut-alist165,4719 -(defconst coq-control-char-format-regexp254,6808 -(defconst coq-control-char-format 258,6933 -(defconst coq-control-characters260,6976 -(defconst coq-control-region-format-regexp 264,7068 -(defconst coq-control-regions266,7151 - -hol98/hol98.el,121 -(defvar hol98-keywords 17,419 -(defvar hol98-rules 18,447 -(defvar hol98-tactics 19,472 -(defvar hol98-tacticals 20,499 - -isar/isabelle-system.el,1255 -(defgroup isabelle 31,882 -(defcustom isabelle-web-page35,1010 -(defcustom isa-isabelle-command44,1227 -(defvar isabelle-not-found 62,1909 -(defun isa-set-isabelle-command 65,2024 -(defun isa-shell-command-to-string 88,3042 -(defun isa-getenv 94,3266 -(defcustom isabelle-program-name-override 114,3965 -(defun isa-tool-list-logics 125,4311 -(defcustom isabelle-logics-available 132,4557 -(defcustom isabelle-chosen-logic 142,4894 -(defvar isabelle-chosen-logic-prev 158,5478 -(defun isabelle-hack-local-variables-function 161,5598 -(defun isabelle-set-prog-name 173,6037 -(defun isabelle-choose-logic 197,7157 -(defun isa-view-doc 216,7919 -(defun isa-tool-list-docs 223,8145 -(defconst isabelle-verbatim-regexp 241,8875 -(defun isabelle-verbatim 244,9017 -(defcustom isabelle-refresh-logics 251,9178 -(defvar isabelle-docs-menu259,9506 -(defvar isabelle-logics-menu-entries 266,9809 -(defun isabelle-logics-menu-calculate 269,9882 -(defvar isabelle-time-to-refresh-logics 290,10524 -(defun isabelle-logics-menu-refresh 294,10619 -(defun isabelle-menu-bar-update-logics 309,11266 -(defun isabelle-load-isar-keywords 325,11895 -(defun isabelle-create-span-menu 346,12623 -(defun isabelle-xml-sml-escapes 362,13054 -(defun isabelle-process-pgip 365,13155 - -isar/isar-autotest.el,31 -(defvar isar-long-tests 8,186 - -isar/isar.el,1595 -(defcustom isar-keywords-name 41,945 -(defpgdefault completion-table 57,1456 -(defcustom isar-web-page59,1509 -(defun isar-strip-terminators 73,1854 -(defun isar-markup-ml 85,2210 -(defun isar-mode-config-set-variables 90,2345 -(defun isar-shell-mode-config-set-variables 155,5144 -(defun isar-set-proof-find-theorems-command 237,8334 -(defpacustom use-find-theorems-form 243,8518 -(defun isar-set-undo-commands 248,8684 -(defpacustom use-linear-undo 263,9317 -(defun isar-configure-from-settings 268,9475 -(defun isar-remove-file 276,9625 -(defun isar-shell-compute-new-files-list 288,9929 -(define-derived-mode isar-shell-mode 307,10499 -(define-derived-mode isar-response-mode 312,10626 -(define-derived-mode isar-goals-mode 317,10759 -(define-derived-mode isar-mode 322,10885 -(defpgdefault menu-entries374,12600 -(defun isar-set-command 405,13794 -(defpgdefault help-menu-entries 410,13924 -(defun isar-count-undos 413,14000 -(defun isar-find-and-forget 439,14966 -(defun isar-goal-command-p 475,16309 -(defun isar-global-save-command-p 480,16486 -(defvar isar-current-goal 501,17270 -(defun isar-state-preserving-p 504,17336 -(defvar isar-shell-current-line-width 529,18185 -(defun isar-shell-adjust-line-width 534,18377 -(defsubst isar-string-wrapping 557,19142 -(defsubst isar-positions-of 566,19336 -(defcustom isar-wrap-commands-singly 572,19541 -(defun isar-command-wrapping 578,19737 -(defun isar-preprocessing 586,20051 -(defun isar-mode-config 604,20602 -(defun isar-shell-mode-config 618,21255 -(defun isar-response-mode-config 628,21604 -(defun isar-goals-mode-config 638,21939 - -isar/isar-find-theorems.el,779 -(defvar isar-find-theorems-data 19,565 -(defun isar-find-theorems-minibuffer 35,1039 -(defun isar-find-theorems-form 49,1658 -(defvar isar-find-theorems-widget-number 92,3532 -(defvar isar-find-theorems-widget-pattern 95,3630 -(defvar isar-find-theorems-widget-intro 98,3722 -(defvar isar-find-theorems-widget-elim 101,3808 -(defvar isar-find-theorems-widget-dest 104,3892 -(defvar isar-find-theorems-widget-name 107,3976 -(defvar isar-find-theorems-widget-simp 110,4063 -(defun isar-find-theorems-create-searchform115,4209 -(defun isar-find-theorems-create-help 255,8752 -(defun isar-find-theorems-submit-searchform298,10924 -(defun isar-find-theorems-parse-criteria 376,13294 -(defun isar-find-theorems-parse-number 469,16275 -(defun isar-find-theorems-filter-empty 479,16552 - -isar/isar-keywords.el,1064 -(defconst isar-keywords-major7,222 -(defconst isar-keywords-minor280,4856 -(defconst isar-keywords-control339,5659 -(defconst isar-keywords-diag360,6153 -(defconst isar-keywords-theory-begin434,7438 -(defconst isar-keywords-theory-switch437,7491 -(defconst isar-keywords-theory-end440,7537 -(defconst isar-keywords-theory-heading443,7585 -(defconst isar-keywords-theory-decl449,7692 -(defconst isar-keywords-theory-script552,9481 -(defconst isar-keywords-theory-goal555,9544 -(defconst isar-keywords-qed583,10059 -(defconst isar-keywords-qed-block590,10145 -(defconst isar-keywords-qed-global593,10192 -(defconst isar-keywords-proof-heading596,10241 -(defconst isar-keywords-proof-goal601,10324 -(defconst isar-keywords-proof-block606,10401 -(defconst isar-keywords-proof-open610,10463 -(defconst isar-keywords-proof-close613,10509 -(defconst isar-keywords-proof-chain616,10556 -(defconst isar-keywords-proof-decl623,10659 -(defconst isar-keywords-proof-asm635,10821 -(defconst isar-keywords-proof-asm-goal642,10916 -(defconst isar-keywords-proof-script648,11005 - -isar/isar-mmm.el,81 -(defconst isar-start-latex-regexp24,744 -(defconst isar-start-sml-regexp36,1172 - -isar/isar-syntax.el,4005 -(defconst isar-script-syntax-table-entries18,483 -(defconst isar-script-syntax-table-alist42,885 -(defun isar-init-syntax-table 51,1168 -(defun isar-init-output-syntax-table 59,1415 -(defconst isar-keyword-begin 74,1857 -(defconst isar-keyword-end 75,1895 -(defconst isar-keywords-theory-enclose77,1930 -(defconst isar-keywords-theory82,2068 -(defconst isar-keywords-save87,2199 -(defconst isar-keywords-proof-enclose92,2314 -(defconst isar-keywords-proof98,2475 -(defconst isar-keywords-proof-context105,2652 -(defconst isar-keywords-local-goal109,2759 -(defconst isar-keywords-proper113,2864 -(defconst isar-keywords-improper118,2983 -(defconst isar-keyword-level-alist123,3115 -(defconst isar-keywords-outline 138,3586 -(defconst isar-keywords-indent-open141,3662 -(defconst isar-keywords-indent-close148,3848 -(defconst isar-keywords-indent-enclose153,3981 -(defconst isar-ext-first 163,4210 -(defconst isar-ext-rest 164,4277 -(defconst isar-text 166,4349 -(defconst isar-long-id-stuff 167,4382 -(defconst isar-id 168,4456 -(defconst isar-idx 169,4526 -(defconst isar-string 171,4585 -(defun isar-ids-to-regexp 173,4645 -(defconst isar-any-command-regexp205,6437 -(defconst isar-name-regexp212,6810 -(defconst isar-improper-regexp218,7105 -(defconst isar-save-command-regexp222,7239 -(defconst isar-global-save-command-regexp225,7340 -(defconst isar-goal-command-regexp228,7454 -(defconst isar-local-goal-command-regexp231,7562 -(defconst isar-comment-start 234,7675 -(defconst isar-comment-end 235,7710 -(defconst isar-comment-start-regexp 236,7743 -(defconst isar-comment-end-regexp 237,7814 -(defconst isar-string-start-regexp 239,7882 -(defconst isar-string-end-regexp 240,7934 -(defun isar-syntactic-context 242,7985 -(defconst isar-antiq-regexp257,8380 -(defconst isar-nesting-regexp263,8531 -(defun isar-nesting 266,8629 -(defun isar-match-nesting 278,9022 -(defface isabelle-string-face 290,9356 -(defface isabelle-quote-face 298,9556 -(defface isabelle-class-name-face306,9752 -(defface isabelle-tfree-name-face314,9939 -(defface isabelle-tvar-name-face322,10132 -(defface isabelle-free-name-face330,10324 -(defface isabelle-bound-name-face338,10512 -(defface isabelle-var-name-face346,10703 -(defconst isabelle-string-face 354,10894 -(defconst isabelle-quote-face 355,10948 -(defconst isabelle-class-name-face 356,11001 -(defconst isabelle-tfree-name-face 357,11063 -(defconst isabelle-tvar-name-face 358,11125 -(defconst isabelle-free-name-face 359,11186 -(defconst isabelle-bound-name-face 360,11247 -(defconst isabelle-var-name-face 361,11309 -(defun isar-font-lock-fontify-syntactically-region 367,11458 -(defvar isar-font-lock-keywords-1402,12736 -(defun isar-output-flkprops 420,13744 -(defun isar-output-flk 426,13996 -(defvar isar-output-font-lock-keywords-1429,14105 -(defun isar-strip-output-markup 453,15104 -(defconst isar-shell-font-lock-keywords457,15240 -(defvar isar-goals-font-lock-keywords460,15324 -(defconst isar-linear-undo 494,16003 -(defconst isar-undo 496,16046 -(defconst isar-pr498,16089 -(defun isar-remove 505,16247 -(defun isar-undos 508,16322 -(defun isar-cannot-undo 518,16556 -(defconst isar-undo-commands521,16626 -(defconst isar-theory-start-regexp529,16763 -(defconst isar-end-regexp535,16921 -(defconst isar-undo-fail-regexp539,17022 -(defconst isar-undo-skip-regexp543,17126 -(defconst isar-undo-ignore-regexp546,17247 -(defconst isar-undo-remove-regexp549,17312 -(defconst isar-keywords-imenu557,17469 -(defconst isar-entity-regexp 564,17660 -(defconst isar-named-entity-regexp567,17756 -(defconst isar-named-entity-name-match-number572,17886 -(defconst isar-generic-expression575,17987 -(defconst isar-indent-any-regexp586,18221 -(defconst isar-indent-inner-regexp588,18314 -(defconst isar-indent-enclose-regexp590,18380 -(defconst isar-indent-open-regexp592,18496 -(defconst isar-indent-close-regexp594,18606 -(defconst isar-outline-regexp600,18743 -(defconst isar-outline-heading-end-regexp 604,18896 -(defconst isar-outline-heading-alist 606,18945 - -isar/isar-unicode-tokens.el,1363 -(defgroup isabelle-tokens 25,672 -(defun isar-set-and-restart-tokens 30,812 -(defconst isar-control-region-format-regexp43,1165 -(defconst isar-control-char-format-regexp46,1259 -(defconst isar-control-char-format 52,1406 -(defconst isar-control-region-format-start 53,1455 -(defconst isar-control-region-format-end 54,1509 -(defcustom isar-control-characters57,1565 -(defcustom isar-control-regions71,1978 -(defconst isar-token-format 97,2790 -(defconst isar-token-variant-format-regexp101,2941 -(defcustom isar-greek-letters-tokens104,3055 -(defcustom isar-misc-letters-tokens144,3913 -(defcustom isar-symbols-tokens156,4231 -(defcustom isar-extended-symbols-tokens362,9042 -(defun isar-try-char 431,10697 -(defcustom isar-symbols-tokens-fallbacks435,10841 -(defcustom isar-bold-nums-tokens462,11771 -(defun isar-map-letters 478,12160 -(defconst isar-script-letters-tokens 484,12308 -(defconst isar-roman-letters-tokens 489,12462 -(defconst isar-fraktur-uppercase-letters-tokens 494,12636 -(defconst isar-fraktur-lowercase-letters-tokens 499,12805 -(defcustom isar-token-symbol-map 504,12996 -(defcustom isar-user-tokens 521,13537 -(defun isar-init-token-symbol-map 535,13977 -(defcustom isar-symbol-shortcuts560,14626 -(defcustom isar-shortcut-alist 632,16825 -(defun isar-init-shortcut-alists 640,17084 -(defconst isar-tokens-customizable-variables661,17747 - -lego/lego.el,1636 -(defcustom lego-tags 21,539 -(defcustom lego-test-all-name 26,675 -(defpgdefault help-menu-entries32,833 -(defpgdefault menu-entries36,993 -(defvar lego-shell-handle-output47,1294 -(defconst lego-process-config55,1604 -(defconst lego-pretty-set-width 66,2035 -(defconst lego-interrupt-regexp 70,2177 -(defcustom lego-www-home-page 75,2294 -(defcustom lego-www-latest-release80,2418 -(defcustom lego-www-refcard86,2593 -(defcustom lego-library-www-page92,2742 -(defvar lego-prog-name 101,2958 -(defvar lego-shell-cd 104,3027 -(defvar lego-shell-proof-completed-regexp 107,3126 -(defvar lego-save-command-regexp110,3266 -(defvar lego-goal-command-regexp112,3356 -(defvar lego-kill-goal-command 115,3447 -(defvar lego-forget-id-command 116,3490 -(defvar lego-undoable-commands-regexp118,3536 -(defvar lego-goal-regexp 127,3910 -(defvar lego-outline-regexp129,3955 -(defvar lego-outline-heading-end-regexp 135,4130 -(defvar lego-shell-outline-regexp 137,4183 -(defvar lego-shell-outline-heading-end-regexp 138,4235 -(define-derived-mode lego-shell-mode 144,4514 -(define-derived-mode lego-mode 151,4675 -(define-derived-mode lego-goals-mode 162,4985 -(defun lego-count-undos 173,5411 -(defun lego-goal-command-p 192,6148 -(defun lego-find-and-forget 197,6319 -(defun lego-goal-hyp 239,8155 -(defun lego-state-preserving-p 248,8352 -(defvar lego-shell-current-line-width 264,9055 -(defun lego-shell-adjust-line-width 272,9362 -(defun lego-mode-config 289,10063 -(defun lego-equal-module-filename 357,12114 -(defun lego-shell-compute-new-files-list 363,12389 -(defun lego-shell-mode-config 373,12772 -(defun lego-goals-mode-config 420,14439 - -lego/lego-syntax.el,600 -(defconst lego-keywords-goal 15,358 -(defconst lego-keywords-save 17,401 -(defconst lego-commands19,472 -(defconst lego-keywords31,1030 -(defconst lego-tacticals 36,1207 -(defconst lego-error-regexp 39,1315 -(defvar lego-id 42,1473 -(defvar lego-ids 44,1500 -(defconst lego-arg-list-regexp 48,1696 -(defun lego-decl-defn-regexp 51,1812 -(defconst lego-definiendum-alternative-regexp59,2184 -(defvar lego-font-lock-terms63,2368 -(defconst lego-goal-with-hole-regexp89,3221 -(defconst lego-save-with-hole-regexp94,3443 -(defvar lego-font-lock-keywords-199,3660 -(defun lego-init-syntax-table 110,4122 - -hol-light/hol-light.el,1930 -(defcustom hol-light-home 23,678 -(defcustom hol-light-prog-name 30,879 -(defcustom hol-light-use-custom-toplevel 38,1075 -(defconst hol-light-pre-sync-cmd52,1571 -(defcustom hol-light-init-cmd 56,1745 -(defconst hol-light-plain-start-goals-regexp78,2476 -(defconst hol-light-annotated-start-goals-regexp 85,2722 -(defconst hol-light-plain-interrupt-regexp89,2881 -(defconst hol-light-annotated-interrupt-regexp93,3012 -(defconst hol-light-plain-prompt-regexp97,3174 -(defconst hol-light-annotated-prompt-regexp101,3328 -(defconst hol-light-plain-error-regexp105,3500 -(defconst hol-light-annotated-error-regexp 116,3825 -(defconst hol-light-plain-proof-completed-regexp121,4046 -(defconst hol-light-annotated-proof-completed-regexp125,4199 -(defconst hol-light-plain-message-start 129,4380 -(defconst hol-light-annotated-message-start133,4524 -(defconst hol-light-plain-message-end137,4678 -(defconst hol-light-annotated-message-end141,4809 -(defvar hol-light-keywords 150,4965 -(defvar hol-light-rules 151,4997 -(defvar hol-light-tactics 152,5026 -(defvar hol-light-tacticals 153,5057 -(defvar hol-light-update-goal-regexp 365,13126 -(defconst hol-light-current-goal-regexp369,13252 -(defconst hol-light-additional-subgoal-regexp 375,13446 -(defconst hol-light-statenumber-regexp 379,13602 -(defconst hol-light-existential-regexp 386,13906 -(defconst hol-light-existentials-state-start-regexp 389,14013 -(defconst hol-light-existentials-state-end-regexp 392,14160 -(defvar proof-shell-delayed-output-start 424,15452 -(defvar proof-shell-delayed-output-end 425,15498 -(defvar proof-info 426,15542 -(defvar proof-action-list 427,15566 -(defun proof-shell-action-list-item 428,15597 -(defconst hol-light-show-sequent-command 430,15648 -(defun hol-light-get-proof-info 432,15716 -(defun hol-light-find-begin-of-unfinished-proof 448,16217 -(defun hol-light-proof-tree-get-new-subgoals 459,16665 -(defpgdefault menu-entries509,18887 - -hol-light/hol-light-unicode-tokens.el,516 -(defconst hol-light-token-format 23,746 -(defconst hol-light-token-match 24,800 -(defconst hol-light-hexcode-match 25,837 -(defun hol-light-unicode-tokens-set 27,877 -(defcustom hol-light-token-symbol-map33,1117 -(defcustom hol-light-shortcut-alist128,3379 -(defconst hol-light-control-char-format-regexp217,5409 -(defconst hol-light-control-char-format 221,5540 -(defconst hol-light-control-characters223,5589 -(defconst hol-light-control-region-format-regexp 227,5687 -(defconst hol-light-control-regions229,5776 - -phox/phox.el,555 -(defcustom phox-prog-name 32,916 -(defcustom phox-web-page37,1018 -(defcustom phox-doc-dir43,1168 -(defcustom phox-lib-dir49,1315 -(defcustom phox-tags-program55,1458 -(defcustom phox-tags-doc61,1637 -(defcustom phox-etags67,1774 -(defpgdefault menu-entries88,2224 -(defun phox-config 102,2417 -(defun phox-shell-config 146,4343 -(define-derived-mode phox-mode 170,5205 -(define-derived-mode phox-shell-mode 186,5668 -(define-derived-mode phox-response-mode 191,5796 -(define-derived-mode phox-goals-mode 201,6157 -(defpgdefault completion-table224,6943 - -phox/phox-extraction.el,383 -(defvar phox-prog-orig 19,619 -(defun phox-prog-flags-modify(21,687 -(defun phox-prog-flags-extract(50,1488 -(defun phox-prog-flags-erase(61,1778 -(defun phox-toggle-extraction(69,1974 -(defun phox-compile-theorem(81,2376 -(defun phox-compile-theorem-on-cursor(87,2601 -(defun phox-output 103,3079 -(defun phox-output-theorem 113,3291 -(defun phox-output-theorem-on-cursor(120,3590 - -phox/phox-font.el,231 -(defvar phox-sym-lock-enabled 1,0 -(defvar phox-sym-lock-color 2,60 -(defvar phox-sym-lock-keywords 3,118 -(defconst phox-font-lock-keywords11,511 -(defconst phox-sym-lock-keywords-table70,2628 -(defun phox-sym-lock-start 93,3202 - -phox/phox-fun.el,1659 -(defconst phox-forget-id-command 11,186 -(defconst phox-forget-proof-command 12,232 -(defconst phox-forget-new-elim-command 13,287 -(defconst phox-forget-new-intro-command 14,345 -(defconst phox-forget-new-equation-command 15,405 -(defconst phox-forget-close-def-command 16,471 -(defconst phox-comments-regexp 18,597 -(defconst phox-strict-comments-regexp 20,776 -(defconst phox-ident-regexp 21,941 -(defconst phox-inductive-option 22,1027 -(defconst phox-spaces-regexp 23,1079 -(defconst phox-sy-definition-regexp 24,1122 -(defconst phox-sy-inductive-regexp 28,1309 -(defconst phox-inductive-regexp 34,1522 -(defconst phox-data-regexp 40,1673 -(defconst phox-definition-regexp 46,1827 -(defconst phox-prove-claim-regexp 50,1971 -(defconst phox-new-elim-regexp 54,2077 -(defconst phox-new-intro-regexp 57,2196 -(defconst phox-new-rewrite-regexp 60,2317 -(defconst phox-new-equation-regexp 63,2442 -(defconst phox-close-def-regexp 66,2569 -(defun phox-init-syntax-table 71,2706 -(defvar phox-top-keywords87,3178 -(defvar phox-proof-keywords135,3633 -(defun phox-find-and-forget 176,3983 -(defalias 'phox-assert-next-command-interactive phox-assert-next-command-interactive255,6399 -(defun phox-depend-theorem(274,7365 -(defun phox-eshow-extlist(283,7654 -(defun phox-flag-name(297,8251 -(defun phox-path(308,8553 -(defun phox-print-expression(319,8789 -(defun phox-print-sort-expression(332,9245 -(defun phox-priority-symbols-list(343,9557 -(defun phox-search-string(355,9929 -(defun phox-constraints(370,10454 -(defun phox-goals(381,10710 -(defvar phox-state-menu393,10919 -(defun phox-delete-symbol(418,11909 -(defun phox-delete-symbol-on-cursor(424,12117 - -phox/phox-lang.el,323 -(defvar phox-lang9,306 -(defun phox-lang-absurd 21,583 -(defun phox-lang-suppress 26,677 -(defun phox-lang-opendef 31,874 -(defun phox-lang-instance 36,992 -(defun phox-lang-open-instance 41,1121 -(defun phox-lang-lock 46,1270 -(defun phox-lang-unlock 51,1400 -(defun phox-lang-prove 56,1536 -(defun phox-lang-let 61,1670 - -phox/phox-outline.el,254 -(defconst phox-outline-title-regexp 19,723 -(defconst phox-outline-section-regexp 20,788 -(defconst phox-outline-save-regexp 21,844 -(defconst phox-outline-heading-end-regexp 38,1387 -(defun phox-outline-level(44,1566 -(defun phox-setup-outline 58,2040 - -phox/phox-pbrpm.el,513 -(defun phox-pbrpm-left-paren-p 39,1671 -(defun phox-pbrpm-right-paren-p 46,1874 -(defun phox-pbrpm-menu-from-string 54,2078 -(defun phox-pbrpm-rename-in-cmd 63,2410 -(defun phox-pbrpm-get-region-name 96,3658 -(defun phox-pbrpm-escape-string 99,3785 -(defun phox-pbrpm-generate-menu 103,3920 -(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu310,11400 -(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p311,11464 -(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p312,11526 - -phox/phox-sym-lock.el,1398 -(defcustom phox-sym-lock-enabled 19,871 -(defvar phox-sym-lock-sym-count 59,2452 -(defvar phox-sym-lock-ext-start 62,2522 -(defvar phox-sym-lock-ext-end 64,2644 -(defvar phox-sym-lock-font-size 67,2763 -(defvar phox-sym-lock-keywords 72,2953 -(defvar phox-sym-lock-enabled 77,3129 -(defvar phox-sym-lock-color 82,3291 -(defvar phox-sym-lock-mouse-face 87,3509 -(defvar phox-sym-lock-mouse-face-enabled 92,3699 -(defconst phox-sym-lock-with-mule 97,3889 -(defun phox-sym-lock-gen-symbol 100,3973 -(defun phox-sym-lock-make-symbols-atomic 108,4275 -(defun phox-sym-lock-compute-font-size 135,5216 -(defvar phox-sym-lock-font-name173,6635 -(defun phox-sym-lock-set-foreground 216,8233 -(defun phox-sym-lock-translate-char 230,8842 -(defun phox-sym-lock-translate-char-or-string 239,9159 -(defun phox-sym-lock-remap-face 246,9387 -(defvar phox-sym-lock-clear-face266,10375 -(defun phox-sym-lock 278,10794 -(defun phox-sym-lock-rec 287,11198 -(defun phox-sym-lock-atom-face 293,11343 -(defun phox-sym-lock-pre-idle-hook-first 298,11639 -(defun phox-sym-lock-pre-idle-hook-last 308,12044 -(defun phox-sym-lock-enable 317,12419 -(defun phox-sym-lock-disable 330,12830 -(defun phox-sym-lock-mouse-face-enable 343,13246 -(defun phox-sym-lock-mouse-face-disable 350,13461 -(defun phox-sym-lock-font-lock-hook 357,13680 -(defun font-lock-set-defaults 372,14371 -(defun phox-sym-lock-patch-keywords 384,14798 - -phox/phox-tags.el,305 -(defun phox-tags-add-table(26,869 -(defun phox-tags-reset-table(35,1264 -(defun phox-tags-add-doc-table(40,1374 -(defun phox-tags-add-lib-table(46,1523 -(defun phox-tags-add-local-table(52,1658 -(defun phox-tags-create-local-table(58,1841 -(defun phox-complete-tag(69,2091 -(defvar phox-tags-menu76,2200 - -generic/pg-assoc.el,81 -(defun proof-associated-buffers 33,973 -(defun proof-associated-windows 43,1183 - -generic/pg-autotest.el,908 -(defvar pg-autotest-success 29,690 -(defvar pg-autotest-log 32,777 -(defun pg-autotest-find-file 37,871 -(defun pg-autotest-find-file-restart 44,1137 -(defmacro pg-autotest-apply 58,1611 -(defmacro pg-autotest 72,2026 -(defun pg-autotest-log 89,2463 -(defun pg-autotest-message 98,2726 -(defun pg-autotest-remark 107,3015 -(defun pg-autotest-timestart 110,3096 -(defun pg-autotest-timetaken 115,3279 -(defun pg-autotest-start 129,3667 -(defun pg-autotest-exit 140,4121 -(defun pg-autotest-test-process-wholefile 160,4904 -(defun pg-autotest-test-script-wholefile 168,5191 -(defun pg-autotest-test-script-randomjumps 193,6123 -(defun pg-autotest-test-retract-file 242,7680 -(defun pg-autotest-test-assert-processed 248,7821 -(defun pg-autotest-test-assert-full 254,8047 -(defun pg-autotest-test-assert-unprocessed 261,8288 -(defun pg-autotest-test-eval 268,8553 -(defun pg-autotest-test-quit-prover 272,8652 - -generic/pg-custom.el,635 -(defpgcustom script-indent 37,1201 -(defconst proof-toolbar-entries-default42,1338 -(defpgcustom toolbar-entries 71,3173 -(defpgcustom prog-args 90,3906 -(defpgcustom prog-env 102,4484 -(defpgcustom quit-timeout 111,4913 -(defpgcustom favourites 123,5340 -(defpgcustom menu-entries 128,5529 -(defpgcustom help-menu-entries 135,5765 -(defpgcustom keymap 142,6028 -(defpgcustom completion-table 147,6199 -(defpgcustom tags-program 158,6575 -(defpgcustom use-holes 167,6959 -(defpgcustom one-command-per-line174,7217 -(defpgcustom maths-menu-enable 185,7453 -(defpgcustom unicode-tokens-enable 191,7633 -(defpgcustom mmm-enable 197,7840 - -generic/pg-goals.el,285 -(define-derived-mode proof-goals-mode 29,736 -(define-key proof-goals-mode-map 56,1612 -(define-key proof-goals-mode-map 58,1728 -(define-key proof-goals-mode-map 59,1796 -(defun proof-goals-config-done 68,1943 -(defun pg-goals-display 76,2209 -(defun pg-goals-button-action 119,3668 - -generic/pg-movie.el,333 -(defconst pg-movie-xml-header 32,923 -(defconst pg-movie-stylesheet34,981 -(defun pg-movie-stylesheet-location 37,1080 -(defvar pg-movie-frame 41,1188 -(defun pg-movie-of-span 43,1242 -(defun pg-movie-of-region 79,2362 -(defun pg-movie-export 86,2550 -(defun pg-movie-export-from 108,3154 -(defun pg-movie-export-directory 119,3475 - -generic/pg-pamacs.el,534 -(defmacro deflocal 35,1138 -(deflocal proof-buffer-type 42,1376 -(defmacro proof-ass-sym 50,1512 -(defmacro proof-ass-symv 56,1771 -(defmacro proof-ass 62,2029 -(defun proof-ass-differs-from-default 68,2281 -(defun proof-defpgcustom-fn 74,2536 -(defun undefpgcustom 98,3420 -(defmacro defpgcustom 104,3644 -(defun proof-defpgdefault-fn 117,4294 -(defmacro defpgdefault 131,4752 -(defmacro defpgfun 142,5114 -(defun proof-defpacustom-fn 156,5513 -(defmacro defpacustom 223,7701 -(defmacro proof-eval-when-ready-for-assistant 270,9510 - -generic/pg-pbrpm.el,1808 -(defvar pg-pbrpm-use-buffer-menu 45,1207 -(defvar pg-pbrpm-start-goal-regexp 48,1329 -(defvar pg-pbrpm-start-goal-regexp-par-num 52,1486 -(defvar pg-pbrpm-end-goal-regexp 55,1609 -(defvar pg-pbrpm-start-hyp-regexp 59,1761 -(defvar pg-pbrpm-start-hyp-regexp-par-num 63,1922 -(defvar pg-pbrpm-start-concl-regexp 67,2129 -(defvar pg-pbrpm-auto-select-regexp 71,2293 -(defvar pg-pbrpm-buffer-menu 78,2454 -(defvar pg-pbrpm-spans 79,2488 -(defvar pg-pbrpm-goal-description 80,2516 -(defvar pg-pbrpm-windows-dialog-bug 81,2555 -(defvar pbrpm-menu-desc 82,2596 -(defun pg-pbrpm-erase-buffer-menu 84,2626 -(defun pg-pbrpm-menu-change-hook 90,2798 -(defun pg-pbrpm-create-reset-buffer-menu 108,3373 -(defun pg-pbrpm-analyse-goal-buffer 127,4215 -(defun pg-pbrpm-button-action 187,6620 -(defun pg-pbrpm-exists 194,6846 -(defun pg-pbrpm-eliminate-id 198,6958 -(defun pg-pbrpm-build-menu 206,7204 -(defun pg-pbrpm-setup-span 269,9524 -(defun pg-pbrpm-run-command 329,11823 -(defun pg-pbrpm-get-pos-info 362,13348 -(defun pg-pbrpm-get-region-info 404,14647 -(defun pg-pbrpm-auto-select-around-point 415,15059 -(defun pg-pbrpm-translate-position 430,15583 -(defun pg-pbrpm-process-click 438,15837 -(defvar pg-pbrpm-remember-region-selected-region 458,16862 -(defvar pg-pbrpm-regions-list 459,16916 -(defun pg-pbrpm-erase-regions-list 461,16952 -(defun pg-pbrpm-filter-regions-list 470,17260 -(defface pg-pbrpm-multiple-selection-face477,17523 -(defface pg-pbrpm-menu-input-face485,17725 -(defun pg-pbrpm-do-remember-region 493,17915 -(defun pg-pbrpm-remember-region-drag-up-hook 514,18763 -(defun pg-pbrpm-remember-region-click-hook 518,18934 -(defun pg-pbrpm-remember-region 523,19119 -(defun pg-pbrpm-process-region 537,19833 -(defun pg-pbrpm-process-regions-list 555,20562 -(defun pg-pbrpm-region-expression 559,20745 - -generic/pg-pgip.el,2932 -(defalias 'pg-pgip-debug pg-pgip-debug39,1091 -(defalias 'pg-pgip-error pg-pgip-error40,1132 -(defalias 'pg-pgip-warning pg-pgip-warning41,1167 -(defconst pg-pgip-version-supported 43,1217 -(defun pg-pgip-process-packet 47,1323 -(defvar pg-pgip-last-seen-id 57,1891 -(defvar pg-pgip-last-seen-seq 58,1925 -(defun pg-pgip-process-pgip 60,1961 -(defun pg-pgip-process-msg 79,2901 -(defvar pg-pgip-post-process-functions94,3492 -(defun pg-pgip-post-process 104,3967 -(defun pg-pgip-process-askpgip 121,4582 -(defun pg-pgip-process-usespgip 127,4786 -(defun pg-pgip-process-usespgml 131,4950 -(defun pg-pgip-process-pgmlconfig 135,5114 -(defun pg-pgip-process-proverinfo 151,5731 -(defun pg-pgip-process-hasprefs 168,6396 -(defun pg-pgip-haspref 182,7028 -(defun pg-pgip-process-prefval 200,7744 -(defun pg-pgip-process-guiconfig 227,8452 -(defvar proof-assistant-idtables 234,8569 -(defun pg-pgip-process-ids 237,8686 -(defun pg-complete-idtable-symbol 263,9758 -(defalias 'pg-pgip-process-setids pg-pgip-process-setids268,9850 -(defalias 'pg-pgip-process-addids pg-pgip-process-addids269,9906 -(defalias 'pg-pgip-process-delids pg-pgip-process-delids270,9962 -(defun pg-pgip-process-idvalue 273,10020 -(defun pg-pgip-process-menuadd 285,10366 -(defun pg-pgip-process-menudel 288,10409 -(defun pg-pgip-process-ready 297,10641 -(defun pg-pgip-process-cleardisplay 300,10682 -(defun pg-pgip-process-proofstate 314,11139 -(defun pg-pgip-process-normalresponse 318,11216 -(defun pg-pgip-process-errorresponse 322,11346 -(defun pg-pgip-process-scriptinsert 326,11475 -(defun pg-pgip-process-metainforesponse 331,11609 -(defun pg-pgip-file-of-url 340,11849 -(defun pg-pgip-process-informfileloaded 345,11984 -(defun pg-pgip-process-informfileretracted 351,12216 -(defun pg-pgip-process-brokerstatus 364,12663 -(defun pg-pgip-process-proveravailmsg 367,12711 -(defun pg-pgip-process-newprovermsg 370,12761 -(defun pg-pgip-process-proverstatusmsg 373,12809 -(defvar pg-pgip-srcids 382,13055 -(defun pg-pgip-process-newfile 386,13162 -(defun pg-pgip-process-filestatus 402,13744 -(defun pg-pgip-process-newobj 422,14398 -(defun pg-pgip-process-delobj 425,14440 -(defun pg-pgip-process-objectstatus 428,14482 -(defun pg-pgip-process-parsescript 442,14834 -(defun pg-pgip-get-pgiptype 465,15708 -(defun pg-pgip-default-for 486,16571 -(defun pg-pgip-subst-for 499,16966 -(defun pg-pgip-interpret-value 512,17336 -(defun pg-pgip-interpret-choice 531,18061 -(defun pg-pgip-string-of-command 562,19078 -(defconst pg-pgip-id579,19839 -(defvar pg-pgip-refseq 585,20119 -(defvar pg-pgip-refid 587,20216 -(defvar pg-pgip-seq 590,20308 -(defun pg-pgip-assemble-packet 592,20372 -(defun pg-pgip-issue 610,21183 -(defun pg-pgip-maybe-askpgip 627,21795 -(defun pg-pgip-askprefs 633,21986 -(defun pg-pgip-askids 637,22100 -(defun pg-pgip-reset 650,22388 -(defconst pg-pgip-start-element-regexp 681,23086 -(defconst pg-pgip-end-element-regexp 682,23138 - -generic/pg-response.el,1254 -(deflocal pg-response-eagerly-raise 32,791 -(define-derived-mode proof-response-mode 42,1016 -(define-key proof-response-mode-map 69,1971 -(define-key proof-response-mode-map 70,2042 -(define-key proof-response-mode-map 71,2096 -(defun proof-response-config-done 75,2182 -(defvar pg-response-special-display-regexp 86,2528 -(defconst proof-multiframe-parameters90,2695 -(defun proof-multiple-frames-enable 99,2985 -(defun proof-three-window-enable 109,3313 -(defun proof-select-three-b 112,3376 -(defun proof-display-three-b 157,4806 -(defvar pg-frame-configuration 167,5174 -(defun pg-cache-frame-configuration 171,5321 -(defun proof-layout-windows 175,5492 -(defun proof-delete-other-frames 241,8163 -(defvar pg-response-erase-flag 272,9251 -(defun pg-response-maybe-erase276,9380 -(defun pg-response-display 320,10843 -(defun pg-response-display-with-face 345,11626 -(defun pg-response-clear-displays 373,12472 -(defun pg-response-message 391,13178 -(defun pg-response-warning 397,13413 -(defun proof-next-error 412,13819 -(defun pg-response-has-error-location 490,16628 -(defcustom proof-trace-buffer-max-lines 505,17047 -(defun proof-trace-buffer-display 512,17282 -(defun proof-trace-buffer-finish 526,17689 -(defun pg-thms-buffer-clear 550,18342 - -generic/pg-user.el,3669 -(defvar which-func-modes)28,748 -(defun proof-script-new-command-advance 43,1241 -(defun proof-maybe-follow-locked-end 69,2268 -(defun proof-goto-command-start 95,3104 -(defun proof-goto-command-end 118,4051 -(defun proof-forward-command 133,4473 -(defun proof-backward-command 154,5194 -(defun proof-goto-point 165,5408 -(defun proof-assert-next-command-interactive 179,5842 -(defun proof-assert-until-point-interactive 191,6328 -(defun proof-process-buffer 198,6573 -(defun proof-undo-last-successful-command 216,7085 -(defun proof-undo-and-delete-last-successful-command 221,7247 -(defun proof-undo-last-successful-command-1 233,7766 -(defun proof-retract-buffer 250,8430 -(defun proof-retract-current-goal 265,9038 -(defun proof-mouse-goto-point 284,9558 -(defvar proof-minibuffer-history 299,9834 -(defun proof-minibuffer-cmd 302,9929 -(defun proof-frob-locked-end 341,11336 -(defmacro proof-if-setting-configured 377,12437 -(defmacro proof-define-assistant-command 385,12706 -(defmacro proof-define-assistant-command-witharg 398,13161 -(defun proof-issue-new-command 418,13983 -(defun proof-cd-sync 458,15206 -(defun proof-electric-terminator-enable 509,16805 -(defun proof-electric-terminator 517,17109 -(defun proof-add-completions 545,18079 -(defun proof-script-complete 568,18902 -(defun pg-copy-span-contents 582,19211 -(defun pg-numth-span-higher-or-lower 596,19635 -(defun pg-control-span-of 622,20381 -(defun pg-move-span-contents 628,20585 -(defun pg-fixup-children-spans 679,22703 -(defun pg-move-region-down 689,22960 -(defun pg-move-region-up 698,23253 -(defun pg-pos-for-event 712,23527 -(defun pg-span-for-event 718,23748 -(defun pg-span-context-menu 722,23892 -(defun pg-toggle-visibility 738,24409 -(defun pg-create-in-span-context-menu 747,24716 -(defun pg-span-undo 772,25744 -(defun pg-goals-buffers-hint 785,25982 -(defun pg-slow-fontify-tracing-hint 789,26200 -(defun pg-response-buffers-hint 793,26389 -(defun pg-jump-to-end-hint 805,26804 -(defun pg-processing-complete-hint 809,26933 -(defun pg-next-error-hint 826,27653 -(defun pg-hint 831,27805 -(defun pg-identifier-under-mouse-query 842,28154 -(defun pg-identifier-near-point-query 853,28478 -(defvar proof-query-identifier-history 882,29401 -(defun proof-query-identifier 885,29488 -(defun pg-identifier-query 896,29844 -(defun proof-imenu-enable 929,30992 -(defvar pg-input-ring 969,32470 -(defvar pg-input-ring-index 972,32527 -(defvar pg-stored-incomplete-input 975,32599 -(defun pg-previous-input 978,32702 -(defun pg-next-input 992,33165 -(defun pg-delete-input 997,33287 -(defun pg-get-old-input 1010,33625 -(defun pg-restore-input 1024,34016 -(defun pg-search-start 1035,34306 -(defun pg-regexp-arg 1047,34798 -(defun pg-search-arg 1059,35246 -(defun pg-previous-matching-input-string-position 1073,35663 -(defun pg-previous-matching-input 1100,36828 -(defun pg-next-matching-input 1119,37678 -(defvar pg-matching-input-from-input-string 1127,38061 -(defun pg-previous-matching-input-from-input 1131,38175 -(defun pg-next-matching-input-from-input 1149,38940 -(defun pg-add-to-input-history 1160,39319 -(defun pg-remove-from-input-history 1172,39772 -(defun pg-clear-input-ring 1183,40152 -(define-key proof-mode-map 1200,40622 -(define-key proof-mode-map 1201,40682 -(defun pg-protected-undo 1203,40754 -(defun pg-protected-undo-1 1233,42048 -(defun next-undo-elt 1264,43485 -(defvar proof-autosend-timer 1291,44441 -(deflocal proof-autosend-modified-tick 1293,44502 -(defun proof-autosend-enable 1297,44624 -(defun proof-autosend-delay 1311,45167 -(defun proof-autosend-loop 1315,45300 -(defun proof-autosend-loop-all 1329,45860 -(defun proof-autosend-loop-next 1353,46640 - -generic/pg-vars.el,1500 -(defvar proof-assistant-cusgrp 22,386 -(defvar proof-assistant-internals-cusgrp 28,646 -(defvar proof-assistant 34,916 -(defvar proof-assistant-symbol 39,1139 -(defvar proof-mode-for-shell 52,1681 -(defvar proof-mode-for-response 57,1871 -(defvar proof-mode-for-goals 62,2097 -(defvar proof-mode-for-script 67,2286 -(defvar proof-ready-for-assistant-hook 72,2463 -(defvar proof-shell-busy 83,2751 -(defvar proof-shell-last-queuemode 101,3422 -(defvar proof-included-files-list 105,3577 -(defvar proof-script-buffer 127,4596 -(defvar proof-previous-script-buffer 130,4688 -(defvar proof-shell-buffer 134,4861 -(defvar proof-goals-buffer 137,4947 -(defvar proof-response-buffer 140,5002 -(defvar proof-trace-buffer 143,5063 -(defvar proof-thms-buffer 147,5217 -(defvar proof-shell-error-or-interrupt-seen 151,5372 -(defvar pg-response-next-error 156,5596 -(defvar proof-shell-proof-completed 159,5703 -(defvar proof-shell-silent 173,6088 -(defvar proof-shell-last-prompt 176,6176 -(defvar proof-shell-last-output 180,6346 -(defvar proof-shell-last-output-kind 184,6486 -(defvar proof-assistant-settings 204,7250 -(defvar pg-tracing-slow-mode 214,7764 -(defvar proof-nesting-depth 217,7853 -(defvar proof-last-theorem-dependencies 224,8088 -(defvar proof-autosend-running 228,8250 -(defvar proof-next-command-on-new-line 233,8449 -(defcustom proof-general-name 244,8683 -(defcustom proof-general-home-page249,8840 -(defcustom proof-unnamed-theorem-name255,9000 -(defcustom proof-universal-keys261,9184 - -generic/pg-xml.el,1177 -(defalias 'pg-xml-error pg-xml-error18,381 -(defun pg-xml-parse-string 41,1023 -(defun pg-xml-parse-buffer 51,1335 -(defun pg-xml-get-attr 70,1950 -(defun pg-xml-child-elts 78,2252 -(defun pg-xml-child-elt 83,2457 -(defun pg-xml-get-child 91,2739 -(defun pg-xml-get-text-content 101,3106 -(defmacro pg-xml-attr 112,3456 -(defmacro pg-xml-node 114,3518 -(defconst pg-xml-header117,3610 -(defun pg-xml-string-of 121,3686 -(defun pg-xml-output-internal 132,4053 -(defun pg-xml-cdata 166,5192 -(defsubst pg-pgip-get-area 174,5385 -(defun pg-pgip-get-icon 177,5502 -(defsubst pg-pgip-get-name 181,5650 -(defsubst pg-pgip-get-version 184,5767 -(defsubst pg-pgip-get-descr 187,5890 -(defsubst pg-pgip-get-thmname 190,6009 -(defsubst pg-pgip-get-thyname 193,6132 -(defsubst pg-pgip-get-url 196,6255 -(defsubst pg-pgip-get-srcid 199,6370 -(defsubst pg-pgip-get-proverid 202,6489 -(defsubst pg-pgip-get-symname 205,6614 -(defsubst pg-pgip-get-prefcat 208,6734 -(defsubst pg-pgip-get-default 211,6862 -(defsubst pg-pgip-get-objtype 214,6985 -(defsubst pg-pgip-get-value 217,7108 -(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext220,7178 -(defun pg-pgip-get-pgmltext 222,7237 - -generic/proof-autoloads.el,97 -(defsubst proof-shell-live-buffer 736,23730 -(defsubst proof-replace-regexp-in-string 892,29291 - -generic/proof-auxmodes.el,149 -(defun proof-mmm-support-available 20,495 -(defun proof-maths-menu-support-available 42,1096 -(defun proof-unicode-tokens-support-available 56,1513 - -generic/proof-config.el,7902 -(defgroup prover-config 80,2634 -(defcustom proof-guess-command-line 98,3484 -(defcustom proof-assistant-home-page 113,3979 -(defcustom proof-context-command 119,4149 -(defcustom proof-info-command 124,4283 -(defcustom proof-showproof-command 131,4554 -(defcustom proof-goal-command 136,4690 -(defcustom proof-save-command 144,4987 -(defcustom proof-find-theorems-command 152,5296 -(defcustom proof-query-identifier-command 159,5604 -(defcustom proof-assistant-true-value 173,6293 -(defcustom proof-assistant-false-value 179,6483 -(defcustom proof-assistant-format-int-fn 185,6677 -(defcustom proof-assistant-format-float-fn 192,6926 -(defcustom proof-assistant-format-string-fn 199,7181 -(defcustom proof-assistant-setting-format 206,7448 -(defcustom proof-tree-configured 216,7931 -(defgroup proof-script 234,8397 -(defcustom proof-terminal-string 239,8527 -(defcustom proof-electric-terminator-noterminator 249,8915 -(defcustom proof-script-sexp-commands 254,9087 -(defcustom proof-script-command-end-regexp 265,9546 -(defcustom proof-script-command-start-regexp 283,10367 -(defcustom proof-script-integral-proofs 294,10830 -(defcustom proof-script-fly-past-comments 309,11486 -(defcustom proof-script-parse-function 314,11657 -(defcustom proof-script-comment-start 332,12302 -(defcustom proof-script-comment-start-regexp 343,12739 -(defcustom proof-script-comment-end 351,13058 -(defcustom proof-script-comment-end-regexp 363,13480 -(defcustom proof-string-start-regexp 371,13793 -(defcustom proof-string-end-regexp 376,13958 -(defcustom proof-case-fold-search 381,14119 -(defcustom proof-save-command-regexp 390,14531 -(defcustom proof-save-with-hole-regexp 395,14641 -(defcustom proof-save-with-hole-result 406,15016 -(defcustom proof-goal-command-regexp 416,15460 -(defcustom proof-goal-with-hole-regexp 424,15747 -(defcustom proof-goal-with-hole-result 436,16190 -(defcustom proof-non-undoables-regexp 445,16568 -(defcustom proof-nested-undo-regexp 456,17031 -(defcustom proof-ignore-for-undo-count 472,17751 -(defcustom proof-script-imenu-generic-expression 480,18062 -(defcustom proof-goal-command-p 488,18401 -(defcustom proof-really-save-command-p 499,18892 -(defcustom proof-completed-proof-behaviour 508,19199 -(defcustom proof-count-undos-fn 536,20548 -(defcustom proof-find-and-forget-fn 548,21099 -(defcustom proof-forget-id-command 565,21808 -(defcustom pg-topterm-goalhyplit-fn 575,22166 -(defcustom proof-kill-goal-command 587,22709 -(defcustom proof-undo-n-times-cmd 601,23213 -(defcustom proof-nested-goals-history-p 615,23750 -(defcustom proof-arbitrary-undo-positions 624,24087 -(defcustom proof-state-preserving-p 638,24668 -(defcustom proof-activate-scripting-hook 648,25140 -(defcustom proof-deactivate-scripting-hook 667,25921 -(defcustom proof-no-fully-processed-buffer 676,26251 -(defcustom proof-script-evaluate-elisp-comment-regexp 687,26749 -(defcustom proof-indent 705,27335 -(defcustom proof-indent-hang 710,27442 -(defcustom proof-indent-enclose-offset 715,27568 -(defcustom proof-indent-open-offset 720,27710 -(defcustom proof-indent-close-offset 725,27847 -(defcustom proof-indent-any-regexp 730,27985 -(defcustom proof-indent-inner-regexp 735,28145 -(defcustom proof-indent-enclose-regexp 740,28299 -(defcustom proof-indent-open-regexp 745,28453 -(defcustom proof-indent-close-regexp 750,28605 -(defcustom proof-script-font-lock-keywords 756,28759 -(defcustom proof-script-syntax-table-entries 764,29111 -(defcustom proof-script-span-context-menu-extensions 782,29507 -(defgroup proof-shell 808,30267 -(defcustom proof-prog-name 818,30437 -(defcustom proof-shell-auto-terminate-commands 830,30904 -(defcustom proof-shell-pre-sync-init-cmd 839,31309 -(defcustom proof-shell-init-cmd 853,31867 -(defcustom proof-shell-init-hook 865,32413 -(defcustom proof-shell-restart-cmd 870,32552 -(defcustom proof-shell-quit-cmd 875,32707 -(defcustom proof-shell-cd-cmd 880,32874 -(defcustom proof-shell-start-silent-cmd 897,33545 -(defcustom proof-shell-stop-silent-cmd 906,33921 -(defcustom proof-shell-silent-threshold 915,34256 -(defcustom proof-shell-inform-file-processed-cmd 923,34590 -(defcustom proof-shell-inform-file-retracted-cmd 944,35518 -(defcustom proof-auto-multiple-files 972,36790 -(defcustom proof-cannot-reopen-processed-files 987,37511 -(defcustom proof-shell-annotated-prompt-regexp 1007,38302 -(defcustom proof-shell-error-regexp 1022,38867 -(defcustom proof-shell-truncate-before-error 1042,39677 -(defcustom pg-next-error-regexp 1056,40216 -(defcustom pg-next-error-filename-regexp 1071,40825 -(defcustom pg-next-error-extract-filename 1095,41858 -(defcustom proof-shell-interrupt-regexp 1102,42101 -(defcustom proof-shell-proof-completed-regexp 1116,42704 -(defcustom proof-shell-clear-response-regexp 1129,43220 -(defcustom proof-shell-clear-goals-regexp 1141,43680 -(defcustom proof-shell-start-goals-regexp 1153,44134 -(defcustom proof-shell-end-goals-regexp 1166,44709 -(defcustom proof-shell-eager-annotation-start 1180,45299 -(defcustom proof-shell-eager-annotation-start-length 1203,46318 -(defcustom proof-shell-eager-annotation-end 1214,46744 -(defcustom proof-shell-strip-output-markup 1230,47419 -(defcustom proof-shell-assumption-regexp 1239,47804 -(defcustom proof-shell-process-file 1249,48208 -(defcustom proof-shell-retract-files-regexp 1275,49284 -(defcustom proof-shell-compute-new-files-list 1288,49772 -(defcustom pg-special-char-regexp 1303,50339 -(defcustom proof-shell-set-elisp-variable-regexp 1308,50483 -(defcustom proof-shell-match-pgip-cmd 1346,52157 -(defcustom proof-shell-issue-pgip-cmd 1360,52647 -(defcustom proof-use-pgip-askprefs 1365,52820 -(defcustom proof-shell-query-dependencies-cmd 1373,53167 -(defcustom proof-shell-theorem-dependency-list-regexp 1380,53427 -(defcustom proof-shell-theorem-dependency-list-split 1396,54095 -(defcustom proof-shell-show-dependency-cmd 1405,54526 -(defcustom proof-shell-trace-output-regexp 1427,55432 -(defcustom proof-shell-thms-output-regexp 1445,56034 -(defcustom proof-shell-interactive-prompt-regexp 1453,56368 -(defcustom proof-tokens-activate-command 1472,57021 -(defcustom proof-tokens-deactivate-command 1479,57261 -(defcustom proof-tokens-extra-modes 1486,57506 -(defcustom proof-shell-unicode 1501,58011 -(defcustom proof-shell-filename-escapes 1510,58401 -(defcustom proof-shell-process-connection-type 1527,59081 -(defcustom proof-shell-strip-crs-from-input 1533,59308 -(defcustom proof-shell-strip-crs-from-output 1545,59791 -(defcustom proof-shell-extend-queue-hook 1553,60159 -(defcustom proof-shell-insert-hook 1563,60589 -(defcustom proof-script-preprocess 1606,62687 -(defcustom proof-shell-handle-delayed-output-hook1612,62838 -(defcustom proof-shell-handle-error-or-interrupt-hook1618,63053 -(defcustom proof-shell-signal-interrupt-hook 1636,63799 -(defcustom proof-shell-pre-interrupt-hook1647,64268 -(defcustom proof-shell-handle-output-system-specific 1655,64539 -(defcustom proof-state-change-hook 1678,65512 -(defcustom proof-shell-syntax-table-entries 1688,65905 -(defgroup proof-goals 1706,66276 -(defcustom pg-subterm-first-special-char 1711,66397 -(defcustom pg-subterm-anns-use-stack 1719,66709 -(defcustom pg-goals-change-goal 1728,67008 -(defcustom pbp-goal-command 1733,67124 -(defcustom pbp-hyp-command 1738,67288 -(defcustom pg-subterm-help-cmd 1743,67458 -(defcustom pg-goals-error-regexp 1750,67702 -(defcustom proof-shell-result-start 1755,67870 -(defcustom proof-shell-result-end 1761,68112 -(defcustom pg-subterm-start-char 1767,68325 -(defcustom pg-subterm-sep-char 1778,68799 -(defcustom pg-subterm-end-char 1784,68978 -(defcustom pg-topterm-regexp 1790,69135 -(defcustom proof-goals-font-lock-keywords 1805,69735 -(defcustom proof-response-font-lock-keywords 1813,70094 -(defcustom proof-shell-font-lock-keywords 1821,70456 -(defcustom pg-before-fontify-output-hook 1832,70970 -(defcustom pg-after-fontify-output-hook 1840,71331 - -generic/proof-depends.el,917 -(defvar proof-thm-names-of-files 25,639 -(defvar proof-def-names-of-files 31,923 -(defun proof-depends-module-name-for-buffer 42,1238 -(defun proof-depends-module-of 52,1679 -(defun proof-depends-names-in-same-file 60,1970 -(defun proof-depends-process-dependencies 79,2578 -(defun proof-dependency-in-span-context-menu 132,4313 -(defun proof-dep-alldeps-menu 155,5203 -(defun proof-dep-make-alldeps-menu 161,5429 -(defun proof-dep-split-deps 179,5924 -(defun proof-dep-make-submenu 198,6590 -(defun proof-make-highlight-depts-menu 209,7001 -(defun proof-goto-dependency 220,7309 -(defun proof-show-dependency 227,7561 -(defconst pg-dep-span-priority 234,7850 -(defconst pg-ordinary-span-priority 235,7886 -(defun proof-highlight-depcs 237,7928 -(defun proof-highlight-depts 248,8394 -(defun proof-depends-save-old-face 260,8904 -(defun proof-depends-restore-old-face 265,9081 -(defun proof-dep-unhighlight 271,9310 - -generic/proof-easy-config.el,193 -(defconst proof-easy-config-derived-modes-table17,605 -(defun proof-easy-config-define-derived-modes 24,1011 -(defun proof-easy-config-check-setup 53,2196 -(defmacro proof-easy-config 85,3526 - -generic/proof-faces.el,1809 -(defgroup proof-faces 29,809 -(defconst pg-defface-window-systems36,989 -(defmacro proof-face-specs 49,1551 -(defface proof-queue-face64,2003 -(defface proof-locked-face72,2278 -(defface proof-declaration-name-face82,2604 -(defface proof-tacticals-name-face91,2890 -(defface proof-tactics-name-face100,3152 -(defface proof-error-face109,3417 -(defface proof-warning-face117,3638 -(defface proof-eager-annotation-face126,3895 -(defface proof-debug-message-face134,4113 -(defface proof-boring-face142,4312 -(defface proof-mouse-highlight-face150,4504 -(defface proof-command-mouse-highlight-face158,4722 -(defface proof-region-mouse-highlight-face166,4961 -(defface proof-highlight-dependent-face174,5203 -(defface proof-highlight-dependency-face182,5410 -(defface proof-active-area-face190,5607 -(defface proof-script-sticky-error-face198,5919 -(defface proof-script-highlight-error-face206,6148 -(defconst proof-face-compat-doc 218,6493 -(defconst proof-queue-face 219,6573 -(defconst proof-locked-face 220,6641 -(defconst proof-declaration-name-face 221,6711 -(defconst proof-tacticals-name-face 222,6801 -(defconst proof-tactics-name-face 223,6887 -(defconst proof-error-face 224,6969 -(defconst proof-script-sticky-error-face 225,7037 -(defconst proof-script-highlight-error-face 226,7133 -(defconst proof-warning-face 227,7235 -(defconst proof-eager-annotation-face 228,7307 -(defconst proof-debug-message-face 229,7397 -(defconst proof-boring-face 230,7481 -(defconst proof-mouse-highlight-face 231,7551 -(defconst proof-command-mouse-highlight-face 232,7639 -(defconst proof-region-mouse-highlight-face 233,7743 -(defconst proof-highlight-dependent-face 234,7845 -(defconst proof-highlight-dependency-face 235,7941 -(defconst proof-active-area-face 236,8039 -(defconst proof-script-error-face 237,8119 - -generic/proof-indent.el,219 -(defun proof-indent-indent 19,449 -(defun proof-indent-offset 28,715 -(defun proof-indent-inner-p 45,1316 -(defun proof-indent-goto-prev 54,1616 -(defun proof-indent-calculate 61,1949 -(defun proof-indent-line 82,2708 - -generic/proof-maths-menu.el,83 -(defun proof-maths-menu-set-global 32,906 -(defun proof-maths-menu-enable 46,1357 - -generic/proof-menu.el,2215 -(defvar proof-display-some-buffers-count 36,820 -(defun proof-display-some-buffers 38,865 -(defun proof-menu-define-keys 95,3006 -(defun proof-menu-define-main 154,5912 -(defvar proof-menu-favourites 163,6097 -(defvar proof-menu-settings 166,6204 -(defun proof-menu-define-specific 170,6293 -(defun proof-assistant-menu-update 213,7555 -(defvar proof-help-menu227,7988 -(defvar proof-show-hide-menu235,8252 -(defvar proof-buffer-menu246,8676 -(defun proof-keep-response-history 312,11125 -(defconst proof-quick-opts-menu320,11435 -(defun proof-quick-opts-vars 546,20709 -(defun proof-quick-opts-changed-from-defaults-p 578,21649 -(defun proof-quick-opts-changed-from-saved-p 582,21754 -(defun proof-set-document-centred 590,21910 -(defun proof-set-non-document-centred 603,22336 -(defun proof-quick-opts-save 622,23047 -(defun proof-quick-opts-reset 627,23215 -(defconst proof-config-menu639,23483 -(defconst proof-advanced-menu646,23662 -(defvar proof-menu664,24346 -(defun proof-main-menu 673,24628 -(defun proof-aux-menu 685,24967 -(defun proof-menu-define-favourites-menu 701,25313 -(defun proof-def-favourite 721,25962 -(defvar proof-make-favourite-cmd-history 748,26955 -(defvar proof-make-favourite-menu-history 751,27040 -(defun proof-save-favourites 754,27126 -(defun proof-del-favourite 759,27274 -(defun proof-read-favourite 776,27830 -(defun proof-add-favourite 800,28604 -(defun proof-menu-define-settings-menu 827,29649 -(defun proof-menu-entry-name 856,30641 -(defun proof-menu-entry-for-setting 866,30991 -(defun proof-settings-vars 889,31629 -(defun proof-settings-changed-from-defaults-p 894,31806 -(defun proof-settings-changed-from-saved-p 898,31912 -(defun proof-settings-save 902,32015 -(defun proof-settings-reset 907,32182 -(defun proof-assistant-invisible-command-ifposs 912,32345 -(defun proof-maybe-askprefs 934,33315 -(defun proof-assistant-settings-cmd 950,33932 -(defun proof-assistant-settings-cmds 958,34215 -(defvar proof-assistant-format-table973,34657 -(defun proof-assistant-format-bool 982,35083 -(defun proof-assistant-format-int 985,35196 -(defun proof-assistant-format-float 988,35288 -(defun proof-assistant-format-string 991,35384 -(defun proof-assistant-format 994,35482 - -generic/proof-mmm.el,70 -(defun proof-mmm-set-global 43,1439 -(defun proof-mmm-enable 58,1978 - -generic/proof-script.el,5814 -(deflocal proof-active-buffer-fake-minor-mode 48,1552 -(deflocal proof-script-buffer-file-name 51,1678 -(deflocal pg-script-portions 58,2088 -(defalias 'proof-active-buffer-fake-minor-modeproof-active-buffer-fake-minor-mode61,2194 -(defun proof-next-element-count 70,2389 -(defun proof-element-id 76,2631 -(defun proof-next-element-id 80,2800 -(deflocal proof-locked-span 116,4104 -(deflocal proof-queue-span 123,4370 -(deflocal proof-overlay-arrow 132,4856 -(defun proof-span-give-warning 138,4983 -(defun proof-span-read-only 144,5163 -(defun proof-strict-read-only 153,5536 -(defsubst proof-set-queue-endpoints 163,5914 -(defun proof-set-overlay-arrow 167,6055 -(defsubst proof-set-locked-endpoints 178,6393 -(defsubst proof-detach-queue 183,6569 -(defsubst proof-detach-locked 188,6708 -(defsubst proof-set-queue-start 195,6933 -(defsubst proof-set-locked-end 199,7059 -(defsubst proof-set-queue-end 211,7529 -(defun proof-init-segmentation 222,7826 -(defun proof-colour-locked 252,9077 -(defun proof-colour-locked-span 259,9350 -(defun proof-sticky-errors 265,9623 -(defun proof-restart-buffers 278,10039 -(defun proof-script-buffers-with-spans 302,10972 -(defun proof-script-remove-all-spans-and-deactivate 312,11328 -(defun proof-script-clear-queue-spans-on-error 316,11518 -(defun proof-script-delete-spans 342,12535 -(defun proof-script-delete-secondary-spans 347,12734 -(defun proof-unprocessed-begin 360,13023 -(defun proof-script-end 368,13277 -(defun proof-queue-or-locked-end 377,13587 -(defun proof-locked-region-full-p 396,14180 -(defun proof-locked-region-empty-p 405,14452 -(defun proof-only-whitespace-to-locked-region-p 409,14602 -(defun proof-in-locked-region-p 419,14951 -(defun proof-goto-end-of-locked 431,15208 -(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 448,15995 -(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 459,16476 -(defun proof-end-of-locked-visible-p 471,17016 -(defconst pg-idioms 490,17609 -(defconst pg-all-idioms 493,17705 -(defun pg-clear-script-portions 497,17826 -(defun pg-remove-element 503,18061 -(defun pg-get-element 511,18364 -(defun pg-add-element 521,18679 -(defun pg-invisible-prop 569,20641 -(defun pg-set-element-span-invisible 574,20842 -(defun pg-toggle-element-span-visibility 587,21408 -(defun pg-open-invisible-span 592,21569 -(defun pg-make-element-invisible 597,21740 -(defun pg-make-element-visible 602,21951 -(defun pg-toggle-element-visibility 607,22145 -(defun pg-show-all-portions 613,22408 -(defun pg-show-all-proofs 635,23152 -(defun pg-hide-all-proofs 640,23280 -(defun pg-add-proof-element 645,23411 -(defun pg-span-name 660,24198 -(defvar pg-span-context-menu-keymap693,25405 -(defun pg-last-output-displayform 700,25643 -(defun pg-set-span-helphighlights 723,26534 -(defun proof-complete-buffer-atomic 786,28681 -(defun proof-register-possibly-new-processed-file815,29951 -(defun proof-query-save-this-buffer-p 861,31825 -(defun proof-inform-prover-file-retracted 866,32050 -(defun proof-auto-retract-dependencies 886,32901 -(defun proof-unregister-buffer-file-name 940,35451 -(defsubst proof-action-completed 986,37276 -(defun proof-protected-process-or-retract 990,37446 -(defun proof-deactivate-scripting-auto 1018,38677 -(defun proof-deactivate-scripting-query-user-action 1027,39035 -(defun proof-deactivate-scripting-choose-action 1071,40544 -(defun proof-deactivate-scripting 1083,40929 -(defun proof-activate-scripting 1180,45052 -(defun proof-toggle-active-scripting 1280,49591 -(defun proof-done-advancing 1319,50836 -(defun proof-done-advancing-comment 1387,53333 -(defun proof-done-advancing-save 1421,54719 -(defun proof-make-goalsave1509,58083 -(defun proof-get-name-from-goal 1527,58948 -(defun proof-done-advancing-autosave 1547,59973 -(defun proof-done-advancing-other 1611,62469 -(defun proof-segment-up-to-parser 1640,63433 -(defun proof-script-generic-parse-find-comment-end 1710,65714 -(defun proof-script-generic-parse-cmdend 1719,66128 -(defun proof-script-generic-parse-cmdstart 1770,68024 -(defun proof-script-generic-parse-sexp 1809,69624 -(defun proof-semis-to-vanillas 1821,70090 -(defun proof-next-command-new-line 1874,71763 -(defun proof-script-next-command-advance 1879,71969 -(defun proof-assert-until-point 1898,72469 -(defun proof-assert-electric-terminator 1914,73140 -(defun proof-assert-semis 1958,74820 -(defun proof-retract-before-change 1972,75581 -(defun proof-insert-pbp-command 1995,76237 -(defun proof-insert-sendback-command 2010,76740 -(defun proof-done-retracting 2036,77643 -(defun proof-setup-retract-action 2071,79097 -(defun proof-last-goal-or-goalsave 2083,79702 -(defun proof-retract-target 2107,80614 -(defun proof-retract-until-point-interactive 2186,83867 -(defun proof-retract-until-point 2195,84274 -(define-derived-mode proof-mode 2253,86415 -(defun proof-script-set-visited-file-name 2289,87797 -(defun proof-script-set-buffer-hooks 2311,88810 -(defun proof-script-kill-buffer-fn 2319,89228 -(defun proof-config-done-related 2351,90545 -(defun proof-generic-goal-command-p 2422,93402 -(defun proof-generic-state-preserving-p 2427,93615 -(defun proof-generic-count-undos 2436,94132 -(defun proof-generic-find-and-forget 2467,95260 -(defconst proof-script-important-settings2518,97032 -(defun proof-config-done 2533,97578 -(defun proof-setup-parsing-mechanism 2605,99856 -(defun proof-setup-imenu 2629,100928 -(deflocal proof-segment-up-to-cache 2666,102210 -(deflocal proof-segment-up-to-cache-start 2670,102353 -(deflocal proof-segment-up-to-cache-end 2671,102398 -(deflocal proof-last-edited-low-watermark 2672,102441 -(defun proof-segment-up-to-using-cache 2674,102489 -(defun proof-segment-cache-contents-for 2702,103609 -(defun proof-script-after-change-function 2719,104191 -(defun proof-script-set-after-change-functions 2731,104698 - -generic/proof-shell.el,4011 -(defvar proof-marker 35,775 -(defvar proof-action-list 38,871 -(defsubst proof-shell-invoke-callback 80,2584 -(defvar proof-second-action-list-active 86,2794 -(defvar proof-shell-last-goals-output 108,3747 -(defvar proof-shell-last-response-output 111,3827 -(defvar proof-shell-delayed-output-start 114,3914 -(defvar proof-shell-delayed-output-end 118,4096 -(defvar proof-shell-delayed-output-flags 122,4276 -(defvar proof-shell-interrupt-pending 125,4401 -(defvar proof-shell-exit-in-progress 130,4625 -(defcustom proof-shell-active-scripting-indicator142,4970 -(defun proof-shell-ready-prover 194,6554 -(defsubst proof-shell-live-buffer 208,7093 -(defun proof-shell-available-p 215,7313 -(defun proof-grab-lock 221,7535 -(defun proof-release-lock 231,7964 -(defcustom proof-shell-fiddle-frames 241,8138 -(defvar proof-shell-filter-active 246,8296 -(defvar proof-shell-filter-was-blocked 249,8380 -(defun proof-shell-set-text-representation 253,8564 -(defun proof-shell-make-associated-buffers 260,8891 -(defun proof-shell-start 276,9557 -(defvar proof-shell-kill-function-hooks 439,15123 -(defun proof-shell-kill-function 442,15221 -(defun proof-shell-clear-state 507,17520 -(defun proof-shell-exit 523,17995 -(defun proof-shell-bail-out 547,18929 -(defun proof-shell-restart 557,19451 -(defvar proof-shell-urgent-message-marker 598,20823 -(defvar proof-shell-urgent-message-scanner 601,20944 -(defun proof-shell-handle-error-output 605,21129 -(defun proof-shell-handle-error-or-interrupt 631,21991 -(defun proof-shell-error-or-interrupt-action 674,23740 -(defun proof-goals-pos 704,25018 -(defun proof-pbp-focus-on-first-goal 709,25229 -(defsubst proof-shell-string-match-safe 721,25645 -(defun proof-shell-handle-immediate-output 725,25806 -(defun proof-interrupt-process 792,28413 -(defun proof-shell-insert 827,29695 -(defun proof-shell-action-list-item 884,31677 -(defun proof-shell-set-silent 889,31919 -(defun proof-shell-start-silent-item 895,32138 -(defun proof-shell-clear-silent 901,32327 -(defun proof-shell-stop-silent-item 907,32549 -(defsubst proof-shell-should-be-silent 913,32738 -(defsubst proof-shell-insert-action-item 925,33311 -(defsubst proof-shell-slurp-comments 929,33486 -(defun proof-add-to-queue 940,33891 -(defun proof-start-queue 996,35997 -(defun proof-extend-queue 1008,36392 -(defun proof-shell-exec-loop 1027,37011 -(defun proof-shell-insert-loopback-cmd 1111,40037 -(defun proof-shell-process-urgent-message 1136,41201 -(defun proof-shell-process-urgent-message-default 1192,43226 -(defun proof-shell-process-urgent-message-trace 1208,43810 -(defun proof-shell-process-urgent-message-retract 1220,44333 -(defun proof-shell-process-urgent-message-elisp 1246,45463 -(defun proof-shell-process-urgent-message-thmdeps 1261,45958 -(defun proof-shell-process-interactive-prompt-regexp 1271,46302 -(defun proof-shell-strip-eager-annotations 1283,46658 -(defun proof-shell-filter-wrapper 1299,47158 -(defun proof-shell-filter 1331,48402 -(defun proof-shell-filter-first-command 1437,52153 -(defun proof-shell-process-urgent-messages 1452,52696 -(defun proof-shell-filter-manage-output 1502,54262 -(defsubst proof-shell-display-output-as-response 1539,55753 -(defun proof-shell-handle-delayed-output 1545,56048 -(defvar pg-last-tracing-output-time 1649,59620 -(defvar pg-last-trace-output-count 1652,59733 -(defconst pg-slow-mode-trigger-count 1655,59818 -(defconst pg-slow-mode-duration 1658,59923 -(defconst pg-fast-tracing-mode-threshold 1661,60005 -(defun pg-tracing-tight-loop 1664,60134 -(defun pg-finish-tracing-display 1688,61166 -(defun proof-shell-wait 1708,61662 -(defun proof-done-invisible 1738,62873 -(defun proof-shell-invisible-command 1744,63043 -(defun proof-shell-invisible-cmd-get-result 1791,64635 -(defun proof-shell-invisible-command-invisible-result 1803,65071 -(defun pg-insert-last-output-as-comment 1823,65572 -(define-derived-mode proof-shell-mode 1842,66044 -(defconst proof-shell-important-settings1879,67079 -(defun proof-shell-config-done 1885,67194 - -generic/proof-site.el,708 -(defconst proof-assistant-table-default36,1211 -(defconst proof-general-short-version78,2415 -(defconst proof-general-version-year 84,2602 -(defgroup proof-general 91,2755 -(defgroup proof-general-internals 96,2863 -(defun proof-home-directory-fn 109,3251 -(defcustom proof-home-directory120,3623 -(defcustom proof-images-directory129,3989 -(defcustom proof-info-directory135,4191 -(defun proof-add-to-load-path 150,4667 -(defcustom proof-assistant-table177,5517 -(defcustom proof-assistants 218,6959 -(defun proof-ready-for-assistant 247,8113 -(defvar proof-general-configured-provers 298,10348 -(defun proof-chose-prover 371,12961 -(defun proofgeneral 376,13093 -(defun proof-visit-example-file 385,13411 - -generic/proof-splash.el,991 -(defcustom proof-splash-enable 34,1009 -(defcustom proof-splash-time 39,1161 -(defcustom proof-splash-contents47,1445 -(defconst proof-splash-startup-msg91,3016 -(defconst proof-splash-welcome 100,3394 -(define-derived-mode proof-splash-mode 103,3498 -(define-key proof-splash-mode-map 109,3672 -(define-key proof-splash-mode-map 110,3724 -(defsubst proof-emacs-imagep 115,3851 -(defun proof-get-image 120,3976 -(defvar proof-splash-timeout-conf 142,4776 -(defun proof-splash-centre-spaces 145,4889 -(defun proof-splash-remove-screen 172,6045 -(defun proof-splash-remove-buffer 189,6701 -(defvar proof-splash-seen 200,7089 -(defun proof-splash-insert-contents 203,7191 -(defun proof-splash-display-screen 243,8321 -(defalias 'pg-about pg-about279,9843 -(defun proof-splash-message 282,9909 -(defun proof-splash-timeout-waiter 295,10367 -(defvar proof-splash-old-frame-title-format 308,10927 -(defun proof-splash-set-frame-titles 310,10977 -(defun proof-splash-unset-frame-titles 319,11292 - -generic/proof-syntax.el,1278 -(defsubst proof-ids-to-regexp 22,516 -(defsubst proof-anchor-regexp 29,754 -(defconst proof-no-regexp 33,859 -(defsubst proof-regexp-alt 36,950 -(defsubst proof-regexp-alt-list 45,1262 -(defsubst proof-re-search-forward-region 49,1397 -(defsubst proof-search-forward 62,1895 -(defsubst proof-replace-regexp-in-string 69,2165 -(defsubst proof-re-search-forward 74,2416 -(defsubst proof-re-search-backward 79,2674 -(defsubst proof-re-search-forward-safe 84,2935 -(defsubst proof-string-match 90,3216 -(defsubst proof-string-match-safe 95,3445 -(defsubst proof-stringfn-match 99,3649 -(defsubst proof-looking-at 106,3912 -(defsubst proof-looking-at-safe 111,4099 -(defun proof-buffer-syntactic-context 120,4312 -(defsubst proof-looking-at-syntactic-context-default 141,5174 -(defun proof-looking-at-syntactic-context 150,5529 -(defun proof-inside-comment 159,5991 -(defun proof-inside-string 165,6164 -(defsubst proof-replace-string 175,6363 -(defsubst proof-replace-regexp 180,6567 -(defsubst proof-replace-regexp-nocasefold 185,6776 -(defvar proof-id 195,7064 -(defsubst proof-ids 201,7284 -(defun proof-zap-commas 208,7536 -(defadvice font-lock-fontify-keywords-region234,8422 -(defun proof-format 250,9018 -(defun proof-format-filename 269,9657 -(defun proof-insert 316,11059 - -generic/proof-toolbar.el,2402 -(defun proof-toolbar-function 34,872 -(defun proof-toolbar-icon 38,1019 -(defun proof-toolbar-enabler 42,1166 -(defun proof-toolbar-make-icon 51,1368 -(defun proof-toolbar-make-toolbar-items 60,1676 -(defvar proof-toolbar-map 86,2537 -(defun proof-toolbar-available-p 89,2636 -(defun proof-toolbar-setup 99,2942 -(defun proof-toolbar-enable 121,3833 -(defalias 'proof-toolbar-undo proof-toolbar-undo154,4891 -(defun proof-toolbar-undo-enable-p 156,4959 -(defalias 'proof-toolbar-delete proof-toolbar-delete163,5117 -(defun proof-toolbar-delete-enable-p 165,5198 -(defalias 'proof-toolbar-home proof-toolbar-home173,5380 -(defalias 'proof-toolbar-next proof-toolbar-next177,5447 -(defun proof-toolbar-next-enable-p 179,5518 -(defalias 'proof-toolbar-goto proof-toolbar-goto185,5634 -(defun proof-toolbar-goto-enable-p 187,5684 -(defalias 'proof-toolbar-retract proof-toolbar-retract192,5769 -(defun proof-toolbar-retract-enable-p 194,5826 -(defalias 'proof-toolbar-use proof-toolbar-use200,5945 -(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p201,5997 -(defalias 'proof-toolbar-prooftree proof-toolbar-prooftree205,6080 -(defalias 'proof-toolbar-restart proof-toolbar-restart209,6165 -(defalias 'proof-toolbar-goal proof-toolbar-goal213,6230 -(defalias 'proof-toolbar-qed proof-toolbar-qed217,6288 -(defun proof-toolbar-qed-enable-p 219,6337 -(defalias 'proof-toolbar-state proof-toolbar-state227,6499 -(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p228,6542 -(defalias 'proof-toolbar-context proof-toolbar-context232,6621 -(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p233,6667 -(defalias 'proof-toolbar-command proof-toolbar-command237,6748 -(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p238,6804 -(defun proof-toolbar-help 242,6909 -(defalias 'proof-toolbar-find proof-toolbar-find248,6989 -(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p249,7041 -(defalias 'proof-toolbar-info proof-toolbar-info253,7116 -(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p254,7171 -(defalias 'proof-toolbar-visibility proof-toolbar-visibility258,7269 -(defun proof-toolbar-visibility-enable-p 260,7329 -(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt265,7443 -(defun proof-toolbar-interrupt-enable-p 266,7504 -(defun proof-toolbar-scripting-menu 274,7657 - -generic/proof-tree.el,3683 -(defgroup proof-tree 99,4376 -(defcustom proof-tree-program 104,4517 -(defcustom proof-tree-arguments 109,4663 -(defgroup proof-tree-internals 119,4823 -(defcustom proof-tree-ignored-commands-regexp 127,5092 -(defcustom proof-tree-navigation-command-regexp 139,5591 -(defcustom proof-tree-cheating-regexp 147,5910 -(defcustom proof-tree-new-layer-command-regexp 156,6307 -(defcustom proof-tree-current-goal-regexp 165,6699 -(defcustom proof-tree-update-goal-regexp 175,7101 -(defcustom proof-tree-additional-subgoal-ID-regexp 187,7670 -(defcustom proof-tree-existential-regexp 195,7989 -(defcustom proof-tree-existentials-state-start-regexp 209,8609 -(defcustom proof-tree-existentials-state-end-regexp 220,9160 -(defcustom proof-tree-branch-finished-regexp 232,9803 -(defcustom proof-tree-get-proof-info 242,10194 -(defcustom proof-tree-extract-instantiated-existentials 266,11235 -(defcustom proof-tree-show-sequent-command 283,11953 -(defcustom proof-tree-find-begin-of-unfinished-proof 297,12575 -(defcustom proof-tree-find-undo-position 308,13138 -(defcustom proof-tree-urgent-action-hook 318,13586 -(defvar proof-tree-external-display 342,14441 -(defvar proof-tree-process 353,14946 -(defconst proof-tree-process-name 356,15035 -(defconst proof-tree-process-buffer-name359,15134 -(defvar proof-tree-process-buffer 363,15291 -(defconst proof-tree-emacs-exec-regexp366,15390 -(defvar proof-tree-last-state 370,15557 -(defvar proof-tree-current-proof 374,15661 -(defvar proof-tree-sequent-hash 379,15842 -(defvar proof-tree-existentials-alist 394,16549 -(defvar proof-tree-existentials-alist-history 405,17048 -(defvar proof-tree-output-marker 414,17267 -(defvar proof-tree-filter-continuation 418,17448 -(defun proof-tree-stop-external-display 425,17802 -(defun proof-tree-handle-proof-tree-undo 432,18065 -(defun proof-tree-insert-script 444,18537 -(defun proof-tree-insert-output 470,19488 -(defun proof-tree-process-filter 487,20174 -(defun proof-tree-process-sentinel 547,22505 -(defun proof-tree-start-process 555,22833 -(defun proof-tree-is-running 592,24292 -(defun proof-tree-ensure-running 597,24453 -(defconst proof-tree-protocol-version 607,24657 -(defun proof-tree-send-message 612,24857 -(defun proof-tree-send-configure 626,25343 -(defun proof-tree-send-goal-state 634,25560 -(defun proof-tree-send-update-sequent 662,26678 -(defun proof-tree-send-switch-goal 675,27115 -(defun proof-tree-send-branch-finished 684,27441 -(defun proof-tree-send-proof-complete 698,27956 -(defun proof-tree-send-undo 706,28205 -(defun proof-tree-send-quit-proof 711,28387 -(defun proof-tree-record-existentials-state 722,28722 -(defun proof-tree-undo-state-var 735,29272 -(defun proof-tree-undo-existentials 754,30053 -(defun proof-tree-delete-existential-assoc 762,30368 -(defun proof-tree-add-existential-assoc 768,30631 -(defun proof-tree-clear-existentials 781,31246 -(defun proof-tree-show-goal-callback 791,31514 -(defun proof-tree-make-show-goal-callback 812,32501 -(defun proof-tree-urgent-action 816,32662 -(defun proof-tree-quit-proof 881,35198 -(defun proof-tree-register-existentials 891,35617 -(defun proof-tree-extract-goals 904,36161 -(defun proof-tree-extract-list 926,37106 -(defun proof-tree-extract-existential-info 949,38076 -(defun proof-tree-handle-proof-progress 970,38967 -(defun proof-tree-handle-navigation 1027,41464 -(defun proof-tree-handle-proof-command 1045,42190 -(defun proof-tree-handle-undo 1061,42893 -(defun proof-tree-update-sequent 1093,44192 -(defun proof-tree-handle-delayed-output 1134,45960 -(defun proof-tree-leave-buffer 1194,48408 -(defun proof-tree-display-current-proof 1206,48691 -(defun proof-tree-external-display-toggle 1238,50032 - -generic/proof-unicode-tokens.el,497 -(defvar proof-unicode-tokens-initialised 31,827 -(defun proof-unicode-tokens-init 34,934 -(defun proof-unicode-tokens-configure 48,1436 -(defun proof-unicode-tokens-mode-if-enabled 60,1882 -(defun proof-unicode-tokens-set-global 66,2081 -(defun proof-unicode-tokens-enable 82,2651 -(defun proof-unicode-tokens-reconfigure 102,3504 -(defun proof-unicode-tokens-configure-prover 128,4392 -(defun proof-unicode-tokens-activate-prover 133,4573 -(defun proof-unicode-tokens-deactivate-prover 140,4819 - -generic/proof-useropts.el,1785 -(defgroup proof-user-options 21,566 -(defun proof-set-value 29,745 -(defcustom proof-electric-terminator-enable 62,1868 -(defcustom proof-next-command-insert-space 74,2400 -(defcustom proof-toolbar-enable 82,2730 -(defcustom proof-imenu-enable 88,2903 -(defcustom pg-show-hints 94,3074 -(defcustom proof-shell-quiet-errors 99,3207 -(defcustom proof-trace-output-slow-catchup 106,3478 -(defcustom proof-strict-state-preserving 116,3975 -(defcustom proof-strict-read-only 129,4584 -(defcustom proof-three-window-enable 142,5163 -(defcustom proof-multiple-frames-enable 161,5911 -(defcustom proof-layout-windows-on-visit-file 171,6306 -(defcustom proof-three-window-mode-policy 180,6690 -(defcustom proof-delete-empty-windows 199,7405 -(defcustom proof-shrink-windows-tofit 210,7936 -(defcustom proof-auto-raise-buffers 217,8208 -(defcustom proof-colour-locked 224,8443 -(defcustom proof-sticky-errors 232,8693 -(defcustom proof-query-file-save-when-activating-scripting239,8910 -(defcustom proof-prog-name-ask255,9630 -(defcustom proof-prog-name-guess261,9790 -(defcustom proof-tidy-response269,10055 -(defcustom proof-keep-response-history283,10518 -(defcustom pg-input-ring-size 293,10906 -(defcustom proof-general-debug 298,11058 -(defcustom proof-use-parser-cache 307,11429 -(defcustom proof-follow-mode 314,11683 -(defcustom proof-auto-action-when-deactivating-scripting 338,12860 -(defcustom proof-rsh-command 366,14042 -(defcustom proof-disappearing-proofs 382,14600 -(defcustom proof-full-annotation 387,14761 -(defcustom proof-output-tooltips 397,15224 -(defcustom proof-minibuffer-messages 408,15731 -(defcustom proof-autosend-enable 416,16040 -(defcustom proof-autosend-delay 422,16220 -(defcustom proof-autosend-all 428,16378 -(defcustom proof-fast-process-buffer 433,16547 - -generic/proof-utils.el,1645 -(defmacro proof-with-current-buffer-if-exists 61,1737 -(defmacro proof-with-script-buffer 70,2114 -(defmacro proof-map-buffers 81,2495 -(defmacro proof-sym 86,2680 -(defsubst proof-try-require 91,2841 -(defun proof-save-some-buffers 104,3172 -(defun proof-save-this-buffer 124,3768 -(defun proof-file-truename 137,4132 -(defun proof-files-to-buffers 141,4314 -(defun proof-buffers-in-mode 149,4553 -(defun pg-save-from-death 163,5003 -(defun proof-define-keys 182,5619 -(defun pg-remove-specials 193,5904 -(defun pg-remove-specials-in-string 203,6240 -(defun proof-safe-split-window-vertically 213,6465 -(defun proof-warn-if-unset 218,6645 -(defun proof-get-window-for-buffer 223,6863 -(defun proof-display-and-keep-buffer 260,8497 -(defun proof-clean-buffer 302,10220 -(defun pg-internal-warning 318,10876 -(defun proof-debug 326,11158 -(defun proof-switch-to-buffer 341,11709 -(defun proof-resize-window-tofit 363,12833 -(defun proof-submit-bug-report 458,16681 -(defun proof-deftoggle-fn 493,18038 -(defmacro proof-deftoggle 508,18704 -(defun proof-defintset-fn 519,19217 -(defmacro proof-defintset 538,20041 -(defun proof-deffloatset-fn 545,20420 -(defmacro proof-deffloatset 561,21134 -(defun proof-defstringset-fn 568,21519 -(defmacro proof-defstringset 581,22145 -(defun proof-escape-keymap-doc 594,22601 -(defmacro proof-defshortcut 598,22755 -(defmacro proof-definvisible 613,23353 -(defun pg-custom-save-vars 640,24282 -(defun pg-custom-reset-vars 656,24926 -(defun proof-locate-executable 669,25263 -(defun pg-current-word-pos 684,25813 -(defsubst proof-shell-strip-output-markup 729,27468 -(defun proof-minibuffer-message 735,27732 - -lib/bufhist.el,1257 -(defun bufhist-ring-update 38,1391 -(defgroup bufhist 47,1713 -(defcustom bufhist-ring-size 51,1794 -(defvar bufhist-ring 56,1905 -(defvar bufhist-ring-pos 59,1979 -(defvar bufhist-lastswitch-modified-tick 62,2058 -(defvar bufhist-read-only-history 65,2164 -(defvar bufhist-saved-mode-line-format 68,2235 -(defvar bufhist-normal-read-only 71,2338 -(defvar bufhist-top-point 74,2432 -(defun bufhist-mode-line-format-entry 77,2522 -(defconst bufhist-minor-mode-map106,3596 -(define-minor-mode bufhist-mode119,4073 -(defun bufhist-get-buffer-contents 141,4954 -(defun bufhist-restore-buffer-contents 150,5296 -(defun bufhist-checkpoint 159,5610 -(defun bufhist-erase-buffer 167,5979 -(defun bufhist-checkpoint-and-erase 178,6350 -(defun bufhist-switch-to-index 184,6536 -(defun bufhist-first 223,8135 -(defun bufhist-last 228,8294 -(defun bufhist-prev 233,8438 -(defun bufhist-next 241,8661 -(defun bufhist-delete 246,8801 -(defun bufhist-clear 258,9342 -(defun bufhist-init 273,9737 -(defun bufhist-exit 301,10746 -(defun bufhist-set-readwrite 311,11010 -(defun bufhist-before-change-function 326,11630 -(define-button-type 'bufhist-nextbufhist-next340,12053 -(define-button-type 'bufhist-prevbufhist-prev344,12150 -(defun bufhist-insert-buttons 351,12362 - -lib/holes.el,2465 -(defvar holes-default-hole 44,1123 -(defvar holes-active-hole 50,1301 -(defgroup holes 60,1498 -(defcustom holes-empty-hole-string 65,1597 -(defcustom holes-empty-hole-regexp 70,1740 -(defface active-hole-face92,2442 -(defface inactive-hole-face102,2858 -(defvar hole-map116,3299 -(defvar holes-mode-map126,3690 -(defun holes-region-beginning-or-nil 172,5427 -(defun holes-region-end-or-nil 176,5563 -(defun holes-copy-active-region 180,5681 -(defun holes-is-hole-p 186,5891 -(defun holes-hole-start-position 190,5983 -(defun holes-hole-end-position 196,6166 -(defun holes-hole-buffer 201,6337 -(defun holes-hole-at 207,6511 -(defun holes-active-hole-exist-p 212,6681 -(defun holes-active-hole-start-position 219,6934 -(defun holes-active-hole-end-position 227,7302 -(defun holes-active-hole-buffer 236,7665 -(defun holes-goto-active-hole 244,7966 -(defun holes-highlight-hole-as-active 253,8225 -(defun holes-highlight-hole 261,8533 -(defun holes-disable-active-hole 269,8820 -(defun holes-set-active-hole 282,9352 -(defun holes-is-in-hole-p 292,9697 -(defun holes-make-hole 296,9835 -(defun holes-make-hole-at 314,10491 -(defun holes-clear-hole 328,10944 -(defun holes-clear-hole-at 337,11202 -(defun holes-map-holes 345,11458 -(defun holes-clear-all-buffer-holes 349,11612 -(defun holes-next 359,11912 -(defun holes-next-after-active-hole 366,12163 -(defun holes-set-active-hole-next 373,12379 -(defun holes-replace-segment 392,12916 -(defun holes-replace 401,13269 -(defun holes-replace-active-hole 429,14447 -(defun holes-replace-update-active-hole 436,14738 -(defun holes-delete-update-active-hole 454,15385 -(defun holes-set-make-active-hole 462,15612 -(defalias 'holes-track-mouse-selection holes-track-mouse-selection477,16166 -(defsubst holes-track-mouse-clicks 478,16224 -(defun holes-mouse-replace-active-hole 482,16334 -(defun holes-destroy-hole 496,16805 -(defsubst holes-hole-at-event 510,17187 -(defun holes-mouse-destroy-hole 514,17287 -(defun holes-mouse-forget-hole 521,17508 -(defun holes-mouse-set-make-active-hole 531,17800 -(defun holes-mouse-set-active-hole 547,18299 -(defun holes-set-point-next-hole-destroy 556,18550 -(defun holes-replace-string-by-holes-backward 582,19531 -(defun holes-skeleton-end-hook 600,20231 -(defconst holes-jump-doc609,20669 -(defun holes-replace-string-by-holes-backward-jump 616,20875 -(define-minor-mode holes-mode 634,21632 -(defun holes-abbrev-complete 729,25114 -(defun holes-insert-and-expand 739,25457 - -lib/local-vars-list.el,276 -(defconst local-vars-list-doc 28,827 -(defun local-vars-list-find 43,1276 -(defun local-vars-list-goto-var 62,2047 -(defun local-vars-list-get-current 88,3094 -(defun local-vars-list-get 109,3944 -(defun local-vars-list-get-safe 130,4653 -(defun local-vars-list-set 135,4847 - -lib/maths-menu.el,242 -(defvar maths-menu-filter-predicate 56,2328 -(defvar maths-menu-tokenise-insert 59,2436 -(defun maths-menu-build-menu 62,2551 -(defvar maths-menu-menu84,3312 -(defvar maths-menu-mode-map344,12870 -(define-minor-mode maths-menu-mode352,13089 - -lib/pg-dev.el,199 -(defconst pg-dev-lisp-font-lock-keywords58,1742 -(defun pg-loadpath 84,2444 -(defun unload-pg 94,2615 -(defun profile-pg 125,3509 -(defun elp-pack-number 155,4616 -(defun pg-bug-references 164,4816 - -lib/pg-fontsets.el,210 -(defcustom pg-fontsets-default-fontset 27,803 -(defvar pg-fontsets-names 32,949 -(defun pg-fontsets-make-fontsetsizes 35,1030 -(defconst pg-fontsets-base-fonts54,1791 -(defun pg-fontsets-make-fontsets 60,1921 - -lib/proof-compat.el,123 -(defvar proof-running-on-win32 32,975 -(defun pg-custom-undeclare-variable 53,1777 -(defmacro save-selected-frame 86,2602 - -lib/scomint.el,788 -(defvar scomint-buffer-maximum-size 19,493 -(defvar scomint-output-filter-functions 24,684 -(defvar scomint-mode-map27,794 -(defvar scomint-last-input-start 33,973 -(defvar scomint-last-input-end 34,1011 -(defvar scomint-last-output-start 35,1047 -(defvar scomint-exec-hook 37,1087 -(define-derived-mode scomint-mode 46,1430 -(defsubst scomint-check-proc 65,2345 -(defun scomint-make-in-buffer 73,2685 -(defun scomint-make 97,3952 -(defun scomint-exec 110,4663 -(defun scomint-exec-1 147,6256 -(defalias 'scomint-send-string scomint-send-string197,8386 -(defun scomint-send-eof 199,8440 -(defun scomint-send-input 208,8673 -(defun scomint-truncate-buffer 234,9569 -(defun scomint-strip-ctrl-m 247,9963 -(defun scomint-output-filter 261,10540 -(defun scomint-interrupt-process 284,11295 - -lib/span.el,1553 -(defalias 'span-start span-start22,609 -(defalias 'span-end span-end23,647 -(defalias 'span-set-property span-set-property24,681 -(defalias 'span-property span-property25,724 -(defalias 'span-make span-make26,763 -(defalias 'span-detach span-detach27,799 -(defalias 'span-set-endpoints span-set-endpoints28,839 -(defalias 'span-buffer span-buffer29,884 -(defun span-read-only-hook 31,925 -(defsubst span-read-only 36,1115 -(defsubst span-read-write 43,1425 -(defsubst span-write-warning 48,1595 -(defsubst span-lt 59,2119 -(defsubst spans-at-point-prop 64,2263 -(defsubst spans-at-region-prop 73,2454 -(defsubst span-at 83,2720 -(defsubst span-delete 87,2846 -(defsubst span-add-delete-action 93,3042 -(defsubst span-mapcar-spans 99,3321 -(defsubst span-mapc-spans 103,3496 -(defsubst span-mapcar-spans-inorder 107,3667 -(defun span-at-before 113,3872 -(defsubst prev-span 130,4596 -(defsubst next-span 136,4749 -(defsubst span-live-p 142,4963 -(defsubst span-raise 148,5129 -(defsubst span-string 152,5262 -(defsubst set-span-properties 157,5422 -(defsubst span-find-span 163,5616 -(defsubst span-at-event 171,5928 -(defun fold-spans 177,6125 -(defsubst span-detached-p 191,6658 -(defsubst set-span-face 195,6774 -(defsubst set-span-keymap 199,6872 -(defsubst span-delete-spans 207,7041 -(defsubst span-property-safe 211,7203 -(defsubst span-set-start 215,7340 -(defsubst span-set-end 219,7472 -(defun span-make-self-removing-span 227,7632 -(defun span-delete-self-modification-hook 237,8000 -(defun span-make-modifying-removing-span 242,8174 - -lib/texi-docstring-magic.el,584 -(defun texi-docstring-magic-find-face 88,3032 -(defun texi-docstring-magic-splice-sep 93,3197 -(defconst texi-docstring-magic-munge-table103,3502 -(defun texi-docstring-magic-untabify 193,7265 -(defun texi-docstring-magic-munge-docstring 200,7463 -(defun texi-docstring-magic-texi 239,8744 -(defun texi-docstring-magic-format-default 252,9184 -(defun texi-docstring-magic-texi-for 268,9817 -(defconst texi-docstring-magic-comment326,11776 -(defun texi-docstring-magic 332,11930 -(defun texi-docstring-magic-face-at-point 366,13009 -(defun texi-docstring-magic-insert-magic 381,13532 - -lib/unicode-chars.el,80 -(defvar unicode-chars-alist12,348 -(defun unicode-chars-list-chars 5051,245975 - -lib/unicode-tokens.el,5902 -(defgroup unicode-tokens-options 58,1844 -(defcustom unicode-tokens-add-help-echo 63,1969 -(defun unicode-tokens-toggle-add-help-echo 68,2136 -(defvar unicode-tokens-token-symbol-map 82,2542 -(defvar unicode-tokens-token-format 101,3201 -(defvar unicode-tokens-token-variant-format-regexp 107,3450 -(defvar unicode-tokens-shortcut-alist 121,3983 -(defvar unicode-tokens-shortcut-replacement-alist 127,4260 -(defvar unicode-tokens-control-region-format-regexp 135,4466 -(defvar unicode-tokens-control-char-format-regexp 142,4834 -(defvar unicode-tokens-control-regions 149,5195 -(defvar unicode-tokens-control-characters 152,5271 -(defvar unicode-tokens-control-char-format 155,5353 -(defvar unicode-tokens-control-region-format-start 158,5466 -(defvar unicode-tokens-control-region-format-end 161,5583 -(defvar unicode-tokens-tokens-customizable-variables 164,5696 -(defconst unicode-tokens-configuration-variables171,5864 -(defun unicode-tokens-config 186,6263 -(defun unicode-tokens-config-var 190,6408 -(defun unicode-tokens-copy-configuration-variables 202,6848 -(defvar unicode-tokens-token-list 230,8064 -(defvar unicode-tokens-hash-table 233,8184 -(defvar unicode-tokens-token-match-regexp 236,8300 -(defvar unicode-tokens-uchar-hash-table 242,8583 -(defvar unicode-tokens-uchar-regexp 246,8770 -(defgroup unicode-tokens-faces 254,8955 -(defconst unicode-tokens-font-family-alternatives264,9257 -(defface unicode-tokens-symbol-font-face279,9776 -(defface unicode-tokens-script-font-face290,10249 -(defface unicode-tokens-fraktur-font-face295,10393 -(defface unicode-tokens-serif-font-face300,10518 -(defface unicode-tokens-sans-font-face305,10655 -(defface unicode-tokens-highlight-face310,10777 -(defconst unicode-tokens-fonts319,11139 -(defconst unicode-tokens-fontsymb-properties328,11356 -(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map356,12977 -(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist374,13529 -(defconst unicode-tokens-font-lock-extra-managed-props387,13860 -(defun unicode-tokens-font-lock-keywords 391,14014 -(defun unicode-tokens-calculate-token-match 424,15385 -(defun unicode-tokens-usable-composition 454,16421 -(defun unicode-tokens-help-echo 467,16800 -(defvar unicode-tokens-show-symbols 472,17002 -(defun unicode-tokens-interpret-composition 475,17116 -(defun unicode-tokens-font-lock-compose-symbol 493,17628 -(defun unicode-tokens-prepend-text-properties-in-match 531,19160 -(defun unicode-tokens-prepend-text-property 545,19738 -(defun unicode-tokens-show-symbols 570,20883 -(defun unicode-tokens-symbs-to-props 578,21193 -(defvar unicode-tokens-show-controls 598,21892 -(defun unicode-tokens-show-controls 601,21983 -(defun unicode-tokens-control-char 613,22496 -(defun unicode-tokens-control-region 622,22935 -(defun unicode-tokens-control-font-lock-keywords 633,23482 -(defvar unicode-tokens-use-shortcuts 644,23806 -(defun unicode-tokens-use-shortcuts 647,23909 -(defun unicode-tokens-map-ordering 663,24505 -(defun unicode-tokens-quail-define-rules 672,24858 -(defun unicode-tokens-insert-token 695,25535 -(defun unicode-tokens-annotate-region 704,25839 -(defun unicode-tokens-insert-control 728,26677 -(defun unicode-tokens-insert-uchar-as-token 738,27126 -(defun unicode-tokens-delete-token-near-point 744,27347 -(defun unicode-tokens-delete-backward-char 756,27788 -(defun unicode-tokens-delete-char 767,28169 -(defun unicode-tokens-delete-backward-1 778,28523 -(defun unicode-tokens-delete-1 795,29119 -(defun unicode-tokens-prev-token 811,29663 -(defun unicode-tokens-rotate-token-forward 819,29960 -(defun unicode-tokens-rotate-token-backward 846,30850 -(defun unicode-tokens-replace-shortcut-match 851,31052 -(defun unicode-tokens-replace-shortcuts 860,31422 -(defun unicode-tokens-replace-unicode-match 874,32021 -(defun unicode-tokens-replace-unicode 881,32322 -(defun unicode-tokens-copy-token 898,32924 -(define-button-type 'unicode-tokens-listunicode-tokens-list905,33145 -(defun unicode-tokens-list-tokens 911,33349 -(defun unicode-tokens-list-shortcuts 950,34533 -(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars968,35171 -(defun unicode-tokens-encode-in-temp-buffer 970,35244 -(defun unicode-tokens-encode 988,35900 -(defun unicode-tokens-encode-str 994,36136 -(defun unicode-tokens-copy 998,36298 -(defun unicode-tokens-paste 1007,36704 -(defvar unicode-tokens-highlight-unicode 1026,37425 -(defconst unicode-tokens-unicode-highlight-patterns1029,37517 -(defun unicode-tokens-highlight-unicode 1033,37686 -(defun unicode-tokens-highlight-unicode-setkeywords 1045,38149 -(defun unicode-tokens-initialise 1057,38518 -(defvar unicode-tokens-mode-map 1077,39189 -(defvar unicode-tokens-display-table1080,39286 -(define-minor-mode unicode-tokens-mode1087,39537 -(defun unicode-tokens-set-font-var 1223,44112 -(defun unicode-tokens-set-font-var-aux 1239,44601 -(defun unicode-tokens-mouse-set-font 1270,45762 -(defsubst unicode-tokens-face-font-sym 1283,46276 -(defun unicode-tokens-set-font-restart 1287,46456 -(defun unicode-tokens-save-fonts 1298,46766 -(defun unicode-tokens-custom-save-faces 1306,47022 -(define-key unicode-tokens-mode-map1323,47478 -(define-key unicode-tokens-mode-map1326,47585 -(defvar unicode-tokens-quail-translation-keymap1334,47844 -(define-key unicode-tokens-quail-translation-keymap1341,48034 -(defun unicode-tokens-quail-delete-last-char 1345,48168 -(define-key unicode-tokens-mode-map 1360,48595 -(define-key unicode-tokens-mode-map 1362,48687 -(define-key unicode-tokens-mode-map1364,48778 -(define-key unicode-tokens-mode-map1366,48884 -(define-key unicode-tokens-mode-map1369,48999 -(define-key unicode-tokens-mode-map1371,49108 -(define-key unicode-tokens-mode-map1373,49216 -(define-key unicode-tokens-mode-map1375,49322 -(defun unicode-tokens-customize-submenu 1383,49446 -(defun unicode-tokens-define-menu 1390,49669 - -contrib/mmm/mmm-auto.el,343 -(defvar mmm-autoloaded-classes67,2676 -(defun mmm-autoload-class 89,3439 -(defvar mmm-changed-buffers-list 129,4992 -(defun mmm-major-mode-change 132,5099 -(defun mmm-check-changed-buffers 145,5620 -(defun mmm-mode-on-maybe 154,5970 -(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks166,6374 -(defun mmm-add-find-file-hook 167,6434 - -contrib/mmm/mmm-class.el,415 -(defun mmm-get-class-spec 42,1296 -(defun mmm-get-class-parameter 59,1939 -(defun mmm-set-class-parameter 63,2105 -(defun* mmm-apply-class75,2455 -(defun* mmm-apply-classes90,3072 -(defun* mmm-apply-all 110,3803 -(defun* mmm-ify124,4250 -(defun* mmm-match-region206,7095 -(defun mmm-match->point 269,9480 -(defun mmm-match-and-verify 284,10050 -(defun mmm-get-form 310,11101 -(defun mmm-default-get-form 321,11576 - -contrib/mmm/mmm-cmds.el,712 -(defun mmm-ify-by-class 41,1210 -(defun mmm-ify-region 63,1822 -(defun mmm-ify-by-regexp75,2243 -(defun mmm-parse-buffer 97,2886 -(defun mmm-parse-region 106,3222 -(defun mmm-parse-block 115,3601 -(defun mmm-get-block 132,4352 -(defun mmm-reparse-current-region 146,4634 -(defun mmm-clear-current-region 167,5210 -(defun mmm-clear-regions 172,5374 -(defun mmm-clear-all-regions 177,5520 -(defun* mmm-end-current-region 185,5680 -(defun mmm-narrow-to-submode-region 220,6928 -(defun mmm-insert-region 239,7542 -(defun mmm-insert-by-key 258,8348 -(defun mmm-get-insertion-spec 342,11613 -(defun mmm-insertion-help 369,12573 -(defun mmm-display-insertion-key 379,12936 -(defun mmm-get-all-insertion-keys 401,13723 - -contrib/mmm/mmm-compat.el,418 -(defvar mmm-xemacs 40,1313 -(defvar mmm-keywords-used49,1616 -(defmacro mmm-regexp-opt 91,2632 -(defvar mmm-evaporate-property110,3281 -(defmacro mmm-set-keymap-default 128,4047 -(defmacro mmm-event-key 137,4489 -(defvar skeleton-positions 146,4708 -(defun mmm-fixup-skeleton 147,4739 -(defmacro mmm-make-temp-buffer 159,5162 -(defvar mmm-font-lock-available-p 172,5558 -(defmacro mmm-set-font-lock-defaults 179,5772 - -contrib/mmm/mmm-cweb.el,228 -(defvar mmm-cweb-section-tags38,1117 -(defvar mmm-cweb-section-regexp41,1164 -(defvar mmm-cweb-c-part-tags44,1254 -(defvar mmm-cweb-c-part-regexp47,1313 -(defun mmm-cweb-in-limbo 50,1397 -(defun mmm-cweb-verify-brief-c 57,1622 - -contrib/mmm/mmm-mason.el,410 -(defvar mmm-mason-perl-tags41,1236 -(defvar mmm-mason-pseudo-perl-tags45,1377 -(defvar mmm-mason-non-perl-tags48,1453 -(defvar mmm-mason-perl-tags-regexp51,1554 -(defvar mmm-mason-pseudo-perl-tags-regexp56,1749 -(defvar mmm-mason-tag-names-regexp61,1966 -(defun mmm-mason-verify-inline 66,2186 -(defun mmm-mason-start-line 156,4838 -(defun mmm-mason-end-line 161,4903 -(defun mmm-mason-set-mode-line 168,4997 - -contrib/mmm/mmm-mode.el,1025 -(defun mmm-mode 101,3867 -(defun mmm-mode-on 140,5372 -(defun mmm-mode-off 183,7156 -(defvar mmm-mode-map 209,7897 -(defvar mmm-mode-prefix-map 212,7972 -(defvar mmm-mode-menu-map 215,8082 -(defun mmm-define-key 218,8173 -(define-key mmm-mode-prefix-map 242,8928 -(define-key mmm-mode-prefix-map 249,9186 -(define-key mmm-mode-map 252,9297 -(define-key mmm-mode-menu-map 255,9399 -(define-key mmm-mode-menu-map 257,9471 -(define-key mmm-mode-menu-map 259,9530 -(define-key mmm-mode-menu-map 261,9611 -(define-key mmm-mode-menu-map 263,9692 -(define-key mmm-mode-menu-map 265,9779 -(define-key mmm-mode-menu-map 268,9873 -(define-key mmm-mode-menu-map 270,9933 -(define-key mmm-mode-menu-map 273,10024 -(define-key mmm-mode-menu-map 275,10084 -(define-key mmm-mode-menu-map 277,10191 -(define-key mmm-mode-menu-map 279,10276 -(define-key mmm-mode-menu-map 282,10362 -(define-key mmm-mode-menu-map 284,10422 -(define-key mmm-mode-menu-map 286,10535 -(define-key mmm-mode-menu-map 288,10620 -(define-key mmm-mode-map 291,10703 - -contrib/mmm/mmm-region.el,1643 -(defsubst mmm-overlay-at 54,1749 -(defun mmm-overlays-at 59,1934 -(defun mmm-included-p 72,2387 -(defun mmm-overlays-containing 112,3876 -(defun mmm-overlays-contained-in 125,4314 -(defun mmm-overlays-overlapping 138,4754 -(defun mmm-sort-overlays 149,5117 -(defvar mmm-current-overlay 158,5359 -(defvar mmm-previous-overlay 163,5574 -(defvar mmm-current-submode 168,5762 -(defvar mmm-previous-submode 173,5962 -(defun mmm-update-current-submode 178,6135 -(defun mmm-set-current-submode 199,6930 -(defun mmm-submode-at 210,7373 -(defun mmm-match-front 219,7648 -(defun mmm-match-back 238,8409 -(defun mmm-front-start 257,9154 -(defun mmm-back-end 265,9458 -(defun mmm-valid-submode-region 278,9805 -(defun* mmm-make-region305,10961 -(defun mmm-make-overlay 431,16311 -(defun mmm-get-face 459,17444 -(defun mmm-clear-overlays 470,17736 -(defun mmm-update-mode-info 486,18201 -(defun mmm-update-submode-region 572,21874 -(defun mmm-add-hooks 589,22604 -(defun mmm-remove-hooks 592,22701 -(defun mmm-get-local-variables-list 598,22828 -(defun mmm-get-locals 618,23524 -(defun mmm-get-saved-local 631,24021 -(defun mmm-set-local-variables 635,24186 -(defun mmm-get-saved-local-variables 646,24564 -(defun mmm-save-changed-local-variables 654,24839 -(defun mmm-clear-local-variables 673,25543 -(defun mmm-enable-font-lock 684,25808 -(defun mmm-update-font-lock-buffer 692,26068 -(defun mmm-refontify-maybe 705,26479 -(defun mmm-submode-changes-in 720,26959 -(defun mmm-regions-in 731,27316 -(defun mmm-regions-alist 745,27794 -(defun mmm-fontify-region 762,28321 -(defun mmm-fontify-region-list 783,29343 -(defun mmm-beginning-of-syntax 805,30091 - -contrib/mmm/mmm-rpm.el,154 -(defconst mmm-rpm-sh-start-tags48,1618 -(defvar mmm-rpm-sh-end-tags53,1842 -(defvar mmm-rpm-sh-start-regexp57,2016 -(defvar mmm-rpm-sh-end-regexp61,2194 - -contrib/mmm/mmm-sample.el,168 -(defvar mmm-here-doc-mode-alist 84,2601 -(defun mmm-here-doc-get-mode 93,3086 -(defun mmm-file-variables-verify 208,6343 -(defun mmm-file-variables-find-back 232,7148 - -contrib/mmm/mmm-univ.el,34 -(defun mmm-univ-get-mode 38,1205 - -contrib/mmm/mmm-utils.el,282 -(defmacro mmm-valid-buffer 42,1332 -(defmacro mmm-save-all 61,1941 -(defun mmm-format-string 74,2223 -(defun mmm-format-matches 85,2661 -(defmacro mmm-save-keyword 108,3419 -(defmacro mmm-save-keywords 116,3746 -(defun mmm-looking-back-at 129,4244 -(defun mmm-make-marker 146,4784 - -contrib/mmm/mmm-vars.el,2668 -(defgroup mmm 104,3283 -(defvar mmm-c-derived-modes111,3393 -(defvar mmm-save-local-variables115,3512 -(defvar mmm-buffer-saved-locals 341,10293 -(defvar mmm-region-saved-locals-defaults 346,10493 -(defvar mmm-region-saved-locals-for-dominant 352,10753 -(defgroup mmm-faces 362,11130 -(defcustom mmm-submode-decoration-level 368,11301 -(defface mmm-init-submode-face 386,12145 -(defface mmm-cleanup-submode-face 390,12285 -(defface mmm-declaration-submode-face 394,12422 -(defface mmm-comment-submode-face 398,12568 -(defface mmm-output-submode-face 402,12721 -(defface mmm-special-submode-face 406,12870 -(defface mmm-code-submode-face 410,13034 -(defface mmm-default-submode-face 414,13173 -(defface mmm-delimiter-face 419,13381 -(defcustom mmm-mode-string 426,13507 -(defcustom mmm-submode-mode-line-format 431,13638 -(defvar mmm-primary-mode-display-name 448,14293 -(defvar mmm-buffer-mode-display-name 453,14507 -(defun mmm-set-mode-line 459,14806 -(defvar mmm-classes 483,15614 -(defvar mmm-global-classes 489,15859 -(defcustom mmm-mode-ext-classes-alist 496,16041 -(defun mmm-add-mode-ext-class 515,16831 -(defcustom mmm-major-mode-preferences524,17156 -(defun mmm-add-to-major-mode-preferences 542,17884 -(defun mmm-ensure-modename 558,18642 -(defun mmm-modename->function 567,18945 -(defcustom mmm-delimiter-mode 581,19394 -(defcustom mmm-mode-prefix-key 591,19663 -(defcustom mmm-command-modifiers 596,19790 -(defcustom mmm-insert-modifiers 610,20423 -(defcustom mmm-use-old-command-keys 625,21101 -(defun mmm-use-old-command-keys 635,21565 -(defcustom mmm-mode-hook 643,21757 -(defun mmm-run-constructed-hook 663,22564 -(defun mmm-run-major-hook 671,22908 -(defun mmm-run-submode-hook 674,22985 -(defvar mmm-class-hooks-run 677,23072 -(defun mmm-run-class-hook 682,23244 -(defvar mmm-primary-mode-entry-hook 687,23416 -(defcustom mmm-major-mode-hook 702,24063 -(defun mmm-run-major-mode-hook 716,24694 -(defcustom mmm-global-mode 729,25235 -(defcustom mmm-never-modes745,25902 -(defvar mmm-set-file-name-for-modes 763,26202 -(defvar mmm-mode 774,26561 -(defvar mmm-primary-mode 782,26769 -(defvar mmm-classes-alist 793,27135 -(defun mmm-add-classes 948,35342 -(defun mmm-add-group 953,35507 -(defun mmm-add-to-group 963,35880 -(defconst mmm-version 977,36307 -(defun mmm-version 980,36372 -(defvar mmm-temp-buffer-name 987,36515 -(defvar mmm-interactive-history 993,36645 -(defun mmm-add-to-history 999,36914 -(defun mmm-clear-history 1002,36997 -(defvar mmm-mode-ext-classes 1010,37182 -(defun mmm-get-mode-ext-classes 1015,37393 -(defun mmm-clear-mode-ext-classes 1024,37720 -(defun mmm-mode-ext-applies 1028,37845 -(defun mmm-get-all-classes 1042,38224 - -doc/ProofGeneral.texi,7245 -@node Top140,3994 -@node Preface179,5193 -@node News for Version 4.3News for Version 4.3205,5857 -@node News for Version 4.2News for Version 4.2218,6246 -@node News for Version 4.1News for Version 4.1231,6702 -@node News for Version 4.0News for Version 4.0242,7009 -@node Future263,7860 -@node Credits292,9195 -@node Introducing Proof GeneralIntroducing Proof General414,13304 -@node Installing Proof GeneralInstalling Proof General469,15284 -@node Quick start guideQuick start guide483,15733 -@node Features of Proof GeneralFeatures of Proof General528,17927 -@node Supported proof assistantsSupported proof assistants634,22471 -@node Prerequisites for this manualPrerequisites for this manual689,24464 -@node Organization of this manualOrganization of this manual733,26083 -@node Basic Script ManagementBasic Script Management759,26911 -@node Walkthrough example in IsabelleWalkthrough example in Isabelle778,27511 -@node Proof scriptsProof scripts1064,38921 -@node Script buffersScript buffers1107,41041 -@node Locked queue and editing regionsLocked queue and editing regions1129,41618 -@node Goal-save sequencesGoal-save sequences1185,43765 -@node Active scripting bufferActive scripting buffer1222,45249 -@node Summary of Proof General buffersSummary of Proof General buffers1295,48882 -@node Script editing commandsScript editing commands1344,51139 -@node Script processing commandsScript processing commands1424,54098 -@node Proof assistant commandsProof assistant commands1553,59528 -@node Toolbar commandsToolbar commands1746,66456 -@node Interrupting during trace outputInterrupting during trace output1771,67415 -@node Advanced Script Management and EditingAdvanced Script Management and Editing1811,69345 -@node Document centred workingDocument centred working1832,69966 -@node Automatic processingAutomatic processing1944,74644 -@node Visibility of completed proofsVisibility of completed proofs1999,76692 -@node Switching between proof scriptsSwitching between proof scripts2054,78632 -@node View of processed files View of processed files 2091,80604 -@node Retracting across filesRetracting across files2151,83655 -@node Asserting across filesAsserting across files2164,84286 -@node Automatic multiple file handlingAutomatic multiple file handling2177,84852 -@node Escaping script managementEscaping script management2202,85886 -@node Editing featuresEditing features2259,87998 -@node Unicode symbols and special layout supportUnicode symbols and special layout support2329,90777 -@node Maths menuMaths menu2371,92335 -@node Unicode Tokens modeUnicode Tokens mode2388,93026 -@node Configuring tokens symbols and shortcutsConfiguring tokens symbols and shortcuts2438,95449 -@node Special layout Special layout 2468,96410 -@node Moving between Unicode and tokensMoving between Unicode and tokens2578,100528 -@node Finding available tokens shortcuts and symbolsFinding available tokens shortcuts and symbols2633,102639 -@node Selecting suitable fontsSelecting suitable fonts2672,103813 -@node Support for other PackagesSupport for other Packages2737,106801 -@node Syntax highlightingSyntax highlighting2767,107637 -@node Imenu and SpeedbarImenu and Speedbar2795,108640 -@node Support for outline modeSupport for outline mode2841,110311 -@node Support for completionSupport for completion2866,111440 -@node Support for tagsSupport for tags2923,113602 -@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing2975,115950 -@node Goals buffer commandsGoals buffer commands2991,116545 -@node Graphical Proof-Tree VisualizationGraphical Proof-Tree Visualization3090,120698 -@node Starting and Stopping Proof-Tree VisualizationStarting and Stopping Proof-Tree Visualization3122,121898 -@node Features of ProoftreeFeatures of Prooftree3150,123055 -@node Prooftree CustomizationProoftree Customization3185,124412 -@node Customizing Proof GeneralCustomizing Proof General3209,125291 -@node Basic optionsBasic options3249,126961 -@node How to customizeHow to customize3273,127731 -@node Display customizationDisplay customization3320,129698 -@node User optionsUser options3519,137654 -@node Changing facesChanging faces3764,146669 -@node Script buffer facesScript buffer faces3786,147544 -@node Goals and response facesGoals and response faces3832,149144 -@node Tweaking configuration settingsTweaking configuration settings3877,150676 -@node Hints and TipsHints and Tips3934,153202 -@node Adding your own keybindingsAdding your own keybindings3953,153803 -@node Using file variablesUsing file variables4017,156417 -@node Using abbreviationsUsing abbreviations4100,159456 -@node LEGO Proof GeneralLEGO Proof General4139,160871 -@node LEGO specific commandsLEGO specific commands4180,162240 -@node LEGO tagsLEGO tags4200,162695 -@node LEGO customizationsLEGO customizations4210,162942 -@node Coq Proof GeneralCoq Proof General4240,163782 -@node Coq-specific commandsCoq-specific commands4257,164179 -@node Using the Coq project fileUsing the Coq project file4280,164687 -@node Multiple File SupportMultiple File Support4314,165955 -@node Automatic Compilation in DetailAutomatic Compilation in Detail4402,169287 -@node Locking AncestorsLocking Ancestors4510,174197 -@node Customizing Coq Multiple File SupportCustomizing Coq Multiple File Support4548,175715 -@node Current LimitationsCurrent Limitations4808,186718 -@node Editing multiple proofsEditing multiple proofs4830,187471 -@node User-loaded tacticsUser-loaded tactics4854,188579 -@node Holes featureHoles feature4918,191053 -@node Proof-Tree VisualizationProof-Tree Visualization4943,192272 -@node Isabelle Proof GeneralIsabelle Proof General4967,193219 -@node Choosing logic and starting isabelleChoosing logic and starting isabelle4993,194095 -@node Isabelle commandsIsabelle commands5062,196896 -@node Isabelle settingsIsabelle settings5205,201088 -@node Isabelle customizationsIsabelle customizations5219,201670 -@node HOL Light Proof GeneralHOL Light Proof General5242,202163 -@node Shell Proof GeneralShell Proof General5289,204142 -@node Obtaining and InstallingObtaining and Installing5325,205601 -@node Obtaining Proof GeneralObtaining Proof General5340,205966 -@node Installing Proof General from tarballInstalling Proof General from tarball5366,206848 -@node Setting the names of binariesSetting the names of binaries5390,207638 -@node Notes for syssiesNotes for syssies5418,208578 -@node Bugs and EnhancementsBugs and Enhancements5494,211575 -@node References5515,212390 -@node History of Proof GeneralHistory of Proof General5555,213413 -@node Old News for 3.0Old News for 3.05649,217578 -@node Old News for 3.1Old News for 3.15719,221272 -@node Old News for 3.2Old News for 3.25745,222444 -@node Old News for 3.3Old News for 3.35806,225447 -@node Old News for 3.4Old News for 3.45825,226344 -@node Old News for 3.5Old News for 3.55847,227399 -@node Old News for 3.6Old News for 3.65851,227456 -@node Old News for 3.7Old News for 3.75856,227556 -@node Function IndexFunction Index5886,229010 -@node Variable IndexVariable Index5890,229086 -@node Keystroke IndexKeystroke Index5894,229166 -@node Concept IndexConcept Index5898,229232 - -doc/PG-adapting.texi,4617 -@node Top137,3997 -@node Introduction175,5147 -@node Future216,6800 -@node Credits252,8396 -@node Beginning with a New ProverBeginning with a New Prover262,8688 -@node Overview of adding a new proverOverview of adding a new prover302,10630 -@node Demonstration instance and easy configurationDemonstration instance and easy configuration384,14250 -@node Major modes used by Proof GeneralMajor modes used by Proof General453,17641 -@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands496,19351 -@node Settings for generic user-level commandsSettings for generic user-level commands511,19897 -@node Menu configurationMenu configuration556,21629 -@node Toolbar configurationToolbar configuration580,22546 -@node Proof Script SettingsProof Script Settings639,24783 -@node Recognizing commands and commentsRecognizing commands and comments662,25395 -@node Recognizing proofsRecognizing proofs799,31848 -@node Recognizing other elementsRecognizing other elements903,36152 -@node Configuring undo behaviourConfiguring undo behaviour966,38631 -@node Nested proofsNested proofs1103,44018 -@node Safe (state-preserving) commandsSafe (state-preserving) commands1143,45644 -@node Activate scripting hookActivate scripting hook1166,46597 -@node Automatic multiple filesAutomatic multiple files1190,47467 -@node Completely asserted buffersCompletely asserted buffers1211,48313 -@node Completions1244,49778 -@node Proof Shell SettingsProof Shell Settings1285,51268 -@node Proof shell commandsProof shell commands1316,52550 -@node Script input to the shellScript input to the shell1493,60314 -@node Settings for matching various output from proof processSettings for matching various output from proof process1563,63518 -@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1690,69074 -@node Hooks and other settingsHooks and other settings1950,80364 -@node Goals Buffer SettingsGoals Buffer Settings2029,83508 -@node Splash Screen SettingsSplash Screen Settings2103,86498 -@node Global ConstantsGlobal Constants2129,87253 -@node Handling Multiple FilesHandling Multiple Files2155,88082 -@node Configuring Editing SyntaxConfiguring Editing Syntax2324,96751 -@node Configuring Font LockConfiguring Font Lock2381,98868 -@node Configuring TokensConfiguring Tokens2457,102580 -@node Configuring Proof-Tree VisualizationConfiguring Proof-Tree Visualization2507,104700 -@node A layered set of proof treesA layered set of proof trees2525,105273 -@node Prerequisites2557,106624 -@node Proof-Tree Display InternalsProof-Tree Display Internals2620,109275 -@node Organization of the CodeOrganization of the Code2638,109765 -@node Communication2734,114028 -@node Guards2763,115292 -@node Urgent and Delayed ActionsUrgent and Delayed Actions2817,117437 -@node Full AnnotationFull Annotation2884,120285 -@node Configuring Prooftree for a New Proof AssistantConfiguring Prooftree for a New Proof Assistant2898,120859 -@node Proof Tree Elisp configurationProof Tree Elisp configuration2910,121191 -@node Prooftree AdaptionProoftree Adaption2931,122021 -@node Writing More Lisp CodeWriting More Lisp Code2951,122700 -@node Default values for generic settingsDefault values for generic settings2968,123345 -@node Adding prover-specific configurationsAdding prover-specific configurations2998,124428 -@node Useful variablesUseful variables3041,125710 -@node Useful functions and macrosUseful functions and macros3056,126209 -@node Internals of Proof GeneralInternals of Proof General3166,130521 -@node Spans3196,131451 -@node Proof General site configurationProof General site configuration3211,131824 -@node Configuration variable mechanismsConfiguration variable mechanisms3294,134942 -@node Global variablesGlobal variables3424,140658 -@node Proof script modeProof script mode3499,143282 -@node Proof shell modeProof shell mode3763,155239 -@node Debugging4373,180807 -@node Plans and IdeasPlans and Ideas4416,181683 -@node Proof by pointing and similar featuresProof by pointing and similar features4437,182405 -@node Granularity of atomic command sequencesGranularity of atomic command sequences4475,184063 -@node Browser mode for script files and theoriesBrowser mode for script files and theories4520,186288 -@node Demonstration InstantiationsDemonstration Instantiations4550,187319 -@node demoisa-easy.el4566,187750 -@node demoisa.el4628,189942 -@node Function IndexFunction Index4782,194862 -@node Variable IndexVariable Index4786,194938 -@node Concept IndexConcept Index4795,195117 - -generic/proof.el,0 - -pghaskell/pghaskell.el,0 - -pghaskell/pghashell.el,0 - -pgocaml/pgocaml.el,0 - -pgshell/pgshell.el,0 - -hol-light/hol-light-autotest.el,0 - -isar/isar-profiling.el,0 - -isar/interface-setup.el,0 - -coq/coq-mmm.el,0 - -coq/coq-autotest.el,0 - -acl2/acl2.el,0 |