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-entries127,5014 (defpgdefault help-menu-entries161,6145 (defpgdefault other-buffers-menu-entries 165,6275 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,6988 (defcustom coq-holes-minor-mode 212,7827 (defun coq-build-abbrev-table-from-db 218,7971 (defun filter-state-preserving 237,8597 (defun filter-state-changing 242,8751 (defface coq-solve-tactics-face249,8972 (defface coq-cheat-face258,9302 (defconst coq-solve-tactics-face 266,9550 (defconst coq-cheat-face 270,9714 coq/coq.el,10447 (defcustom coq-prog-name61,2024 (defcustom coq-translate-to-v8 80,2875 (defun coq-build-prog-args 85,2990 (defcustom coq-compiler95,3313 (defcustom coq-dependency-analyzer101,3450 (defcustom coq-use-makefile 107,3590 (defcustom coq-default-undo-limit 113,3762 (defconst coq-shell-init-cmd118,3890 (defcustom coq-prog-env 127,4217 (defconst coq-shell-restart-cmd 135,4466 (defvar coq-shell-prompt-pattern137,4520 (defvar coq-shell-cd 145,4823 (defvar coq-shell-proof-completed-regexp 149,4983 (defvar coq-goal-regexp152,5198 (defun get-coq-library-directory 157,5290 (defconst coq-library-directory 163,5477 (defcustom coq-tags 166,5604 (defconst coq-interrupt-regexp 171,5752 (defcustom coq-www-home-page 174,5845 (defcustom coq-end-goals-regexp-show-subgoals 179,5952 (defcustom coq-end-goals-regexp-hide-subgoals186,6236 (defgroup coq-proof-tree 197,6568 (defcustom coq-proof-tree-ignored-commands-regexp202,6708 (defcustom coq-navigation-command-regexp208,6885 (defcustom coq-proof-tree-cheating-regexp214,7057 (defcustom coq-proof-tree-current-goal-regexp220,7197 (defcustom coq-proof-tree-update-goal-regexp227,7458 (defcustom coq-proof-tree-additional-subgoal-ID-regexp234,7692 (defcustom coq-proof-tree-existential-regexp 240,7890 (defcustom coq-proof-tree-instantiated-existential-regexp245,8044 (defcustom coq-proof-tree-existentials-state-start-regexp251,8264 (defcustom coq-proof-tree-existentials-state-end-regexp 257,8454 (defcustom coq-proof-tree-proof-finished-regexp262,8623 (defvar coq-outline-regexp274,8892 (defvar coq-outline-heading-end-regexp 283,9166 (defvar coq-shell-outline-regexp 285,9220 (defvar coq-shell-outline-heading-end-regexp 286,9270 (defconst coq-state-preserving-tactics-regexp289,9334 (defconst coq-state-changing-commands-regexp291,9436 (defconst coq-state-preserving-commands-regexp293,9545 (defconst coq-commands-regexp295,9658 (defvar coq-retractable-instruct-regexp297,9737 (defvar coq-non-retractable-instruct-regexp299,9829 (defcustom coq-use-smie 331,10525 (defconst coq-script-command-end-regexp 356,11363 (defun coq-script-parse-function 365,11792 (defun coq-set-undo-limit 372,12018 (defun build-list-id-from-string 376,12148 (defun coq-last-prompt-info 385,12623 (defun coq-last-prompt-info-safe 403,13517 (defvar coq-last-but-one-statenum 411,13870 (defvar coq-last-but-one-proofnum 418,14167 (defvar coq-last-but-one-proofstack 421,14265 (defsubst coq-get-span-statenum 424,14375 (defsubst coq-get-span-proofnum 428,14490 (defsubst coq-get-span-proofstack 432,14605 (defsubst coq-set-span-statenum 436,14749 (defsubst coq-get-span-goalcmd 440,14880 (defsubst coq-set-span-goalcmd 444,14994 (defsubst coq-set-span-proofnum 448,15124 (defsubst coq-set-span-proofstack 452,15255 (defsubst proof-last-locked-span 456,15415 (defun proof-clone-buffer 460,15549 (defun proof-store-buffer-win 474,16086 (defun proof-store-response-win 485,16579 (defun proof-store-goals-win 489,16706 (defun coq-set-state-infos 501,17238 (defun count-not-intersection 539,19328 (defun coq-find-and-forget 569,20580 (defvar coq-current-goal 596,21885 (defun coq-goal-hyp 599,21950 (defun coq-state-preserving-p 612,22430 (defun coq-hide-additional-subgoals-switch 622,22724 (defconst notation-print-kinds-table634,23065 (defun coq-PrintScope 638,23232 (defun coq-guess-or-ask-for-string 656,23781 (defun coq-ask-do 670,24321 (defun coq-flag-is-on-p 679,24704 (defun coq-command-with-set-unset 685,24911 (defun coq-ask-do-set-unset 696,25561 (defun coq-ask-do-show-implicits 706,26091 (defun coq-ask-do-show-all 714,26451 (defsubst coq-put-into-brackets 735,27132 (defsubst coq-put-into-quotes 738,27193 (defun coq-SearchIsos 741,27252 (defun coq-SearchConstant 749,27491 (defun coq-Searchregexp 753,27584 (defun coq-SearchRewrite 759,27725 (defun coq-SearchAbout 763,27822 (defun coq-Print 769,27965 (defun coq-Print-with-implicits 777,28235 (defun coq-Print-with-all 782,28389 (defun coq-About 787,28531 (defun coq-About-with-implicits 794,28738 (defun coq-About-with-all 799,28887 (defun coq-LocateConstant 805,29025 (defun coq-LocateLibrary 810,29128 (defun coq-LocateNotation 815,29245 (defun coq-Pwd 823,29476 (defun coq-Inspect 828,29600 (defun coq-PrintSection(832,29700 (defun coq-Print-implicit 836,29793 (defun coq-Check 841,29944 (defun coq-Check-show-implicits 849,30198 (defun coq-Check-show-all 854,30336 (defun coq-Show 859,30462 (defun coq-Show-with-implicits 867,30746 (defun coq-Show-with-all 872,30902 (defun coq-Compile 886,31363 (defun coq-guess-command-line 898,31681 (defpacustom use-editing-holes 935,33238 (defun coq-mode-config 944,33541 (defun coq-shell-mode-config 1059,37788 (defun coq-goals-mode-config 1150,41586 (defun coq-response-config 1157,41830 (defpacustom hide-additional-subgoals 1180,42547 (defpacustom print-fully-explicit 1190,42857 (defpacustom print-implicit 1195,43005 (defpacustom print-coercions 1200,43171 (defpacustom print-match-wildcards 1205,43315 (defpacustom print-elim-types 1210,43495 (defpacustom printing-depth 1215,43661 (defpacustom undo-depth 1220,43822 (defpacustom time-commands 1225,43988 (defgroup coq-auto-compile 1236,44238 (defpacustom compile-before-require 1241,44389 (defcustom coq-compile-command 1253,44881 (defconst coq-compile-substitution-list1283,46164 (defcustom coq-load-path 1303,47085 (defcustom coq-compile-auto-save 1340,48830 (defcustom coq-lock-ancestors 1365,49888 (defpacustom confirm-external-compilation 1374,50209 (defcustom coq-load-path-include-current 1383,50516 (defcustom coq-compile-ignored-directories 1392,50834 (defcustom coq-compile-ignore-library-directory 1405,51467 (defcustom coq-coqdep-error-regexp1417,51955 (defconst coq-require-command-regexp1434,52734 (defconst coq-require-id-regexp1441,53091 (defvar coq-compile-history 1449,53525 (defvar coq-compile-response-buffer 1452,53609 (defvar coq-debug-auto-compilation 1456,53744 (defun time-less-or-equal 1462,53852 (defun coq-max-dep-mod-time 1470,54190 (defun coq-load-path-safep 1493,54988 (defun coq-prog-args 1515,55642 (defun coq-lock-ancestor 1524,55901 (defun coq-unlock-ancestor 1540,56676 (defun coq-unlock-all-ancestors-of-span 1547,56971 (defun coq-compile-ignore-file 1554,57267 (defun coq-library-src-of-obj-file 1578,58154 (defun coq-option-of-load-path-entry 1583,58386 (defun coq-include-options 1597,58901 (defun coq-init-compile-response-buffer 1619,59821 (defun coq-display-compile-response-buffer 1642,60893 (defun coq-get-library-dependencies 1656,61527 (defun coq-compile-library 1708,63922 (defun coq-compile-library-if-necessary 1735,65133 (defun coq-make-lib-up-to-date 1781,67005 (defun coq-auto-compile-externally 1837,69468 (defun coq-map-module-id-to-obj-file 1880,71614 (defun coq-check-module 1933,74216 (defvar coq-process-require-current-buffer1961,75658 (defun coq-compile-save-buffer-filter 1967,75923 (defun coq-compile-save-some-buffers 1977,76337 (defun coq-preprocess-require-commands 1999,77239 (defun coq-switch-buffer-kill-proof-shell 2032,78808 (defun coq-proof-tree-get-proof-info 2052,79441 (defun coq-extract-instantiated-existentials 2062,79829 (defun coq-show-sequent-command 2071,80221 (defun coq-proof-tree-get-new-subgoals 2075,80375 (defun coq-find-begin-of-unfinished-proof 2119,82500 (defun coq-preprocessing 2144,83514 (defun coq-fake-constant-markup 2158,83969 (defun coq-create-span-menu 2174,84574 (defconst module-kinds-table2192,85087 (defconst modtype-kinds-table2196,85236 (defun coq-postfix-.v-p 2200,85365 (defun coq-directories-files 2203,85426 (defun coq-remove-dot-v-extension 2209,85654 (defun coq-load-path-to-paths 2212,85715 (defun coq-build-accessible-modules-list 2215,85794 (defun coq-insert-section-or-module 2222,86111 (defconst reqkinds-kinds-table2244,86991 (defun coq-insert-requires 2248,87148 (defun coq-end-Section 2262,87701 (defun coq-insert-intros 2280,88279 (defun coq-insert-infoH-hook 2292,88810 (defun coq-insert-as 2297,89018 (defun coq-insert-match 2314,89710 (defun coq-insert-solve-tactic 2343,90879 (defun coq-insert-tactic 2349,91130 (defun coq-insert-tactical 2355,91332 (defun coq-insert-command 2361,91563 (defun coq-insert-term 2366,91728 (define-key coq-keymap 2372,91911 (define-key coq-keymap 2373,91969 (define-key coq-keymap 2374,92026 (define-key coq-keymap 2375,92095 (define-key coq-keymap 2376,92151 (define-key coq-keymap 2377,92209 (define-key coq-keymap 2378,92259 (define-key coq-keymap 2379,92332 (define-key coq-keymap 2380,92389 (define-key coq-keymap 2381,92452 (define-key coq-keymap 2384,92530 (define-key coq-keymap 2385,92579 (define-key coq-keymap 2386,92634 (define-key coq-keymap 2387,92686 (define-key coq-keymap 2388,92741 (define-key coq-keymap 2389,92791 (define-key coq-keymap 2390,92841 (define-key coq-keymap 2391,92897 (define-key coq-keymap 2392,92947 (define-key coq-keymap 2393,92991 (define-key coq-keymap 2394,93050 (define-key coq-goals-mode-map 2402,93318 (define-key coq-goals-mode-map 2403,93400 (define-key coq-goals-mode-map 2404,93482 (define-key coq-goals-mode-map 2405,93569 (define-key coq-goals-mode-map 2406,93651 (define-key coq-goals-mode-map 2407,93739 (define-key coq-goals-mode-map 2408,93820 (define-key coq-goals-mode-map 2409,93907 (define-key coq-goals-mode-map 2410,93991 (define-key coq-response-mode-map 2413,94069 (define-key coq-response-mode-map 2414,94154 (define-key coq-response-mode-map 2415,94239 (define-key coq-response-mode-map 2416,94329 (define-key coq-response-mode-map 2417,94414 (define-key coq-response-mode-map 2418,94505 (define-key coq-response-mode-map 2419,94589 (define-key coq-response-mode-map 2420,94689 (define-key coq-response-mode-map 2421,94786 (defvar last-coq-error-location 2428,94936 (defun coq-get-last-error-location 2436,95320 (defun coq-highlight-error 2486,97883 (defun coq-highlight-error-hook 2514,98964 (defun coq-first-word-before 2524,99181 (defun coq-get-from-to-paren 2534,99512 (defun coq-show-first-goal 2547,99918 (defvar coq-modeline-string2 2563,100583 (defvar coq-modeline-string1 2564,100617 (defvar coq-modeline-string0 2565,100651 (defun coq-build-subgoals-string 2566,100692 (defun coq-update-minor-mode-alist 2572,100876 (defun is-not-split-vertic 2606,102441 (defun optim-resp-windows 2615,102881 coq/coq-indent.el,2698 (defconst coq-any-command-regexp20,368 (defconst coq-indent-inner-regexp23,442 (defconst coq-comment-start-regexp 33,804 (defconst coq-comment-end-regexp 34,847 (defconst coq-comment-start-or-end-regexp35,888 (defconst coq-indent-open-regexp37,996 (defconst coq-indent-close-regexp42,1193 (defconst coq-indent-closepar-regexp 48,1392 (defconst coq-indent-closematch-regexp 49,1437 (defconst coq-indent-openpar-regexp 50,1508 (defconst coq-indent-openmatch-regexp 51,1552 (defconst coq-tacticals-tactics-regex52,1632 (defconst coq-indent-any-regexp54,1751 (defconst coq-indent-kw58,1967 (defconst coq-indent-pattern-regexp 68,2433 (defun coq-indent-goal-command-p 72,2536 (defconst coq-period-end-command93,3554 (defconst coq-curlybracket-end-command99,3836 (defconst coq-bullet-end-command104,4065 (defconst coq-end-command-regexp117,4520 (defun coq-search-comment-delimiter-forward 133,5245 (defun coq-search-comment-delimiter-backward 142,5575 (defun coq-skip-until-one-comment-backward 149,5849 (defun coq-skip-until-one-comment-forward 164,6556 (defun coq-looking-at-comment 175,7074 (defun coq-find-comment-start 180,7239 (defun coq-find-comment-end 192,7716 (defun coq-looking-at-syntactic-context 204,8209 (defconst coq-end-command-or-comment-regexp210,8431 (defconst coq-end-command-or-comment-start-regexp213,8540 (defun coq-find-not-in-comment-backward 216,8657 (defun coq-find-not-in-comment-forward 235,9536 (defun coq-is-on-ending-context 261,10728 (defun coq-empty-command-p 270,10941 (defun coq-script-parse-cmdend-forward 285,11682 (defun coq-script-parse-cmdend-backward 337,14183 (defun coq-find-current-start 378,16104 (defun coq-find-real-start 387,16430 (defun same-line 393,16648 (defun coq-command-at-point 396,16735 (defun coq-commands-at-line 411,17346 (defun coq-indent-only-spaces-on-line 435,18312 (defun coq-indent-find-reg 441,18589 (defun coq-find-no-syntactic-on-line 455,19125 (defun coq-back-to-indentation-prevline 468,19598 (defun coq-find-unclosed 514,21665 (defun coq-find-at-same-level-zero 544,22975 (defun coq-find-unopened 573,24241 (defun coq-find-last-unopened 616,25675 (defun coq-end-offset 627,26072 (defun coq-add-iter 652,26842 (defun coq-goal-count 655,26948 (defun coq-save-count 657,27020 (defun coq-proof-count 662,27222 (defun coq-goal-save-diff-maybe-proof 668,27510 (defun coq-indent-command-offset 678,27804 (defun coq-indent-expr-offset 744,30985 (defun coq-indent-comment-offset 863,35867 (defun coq-indent-offset 895,37319 (defun coq-indent-calculate 914,38193 (defun coq-indent-line 917,38281 (defun coq-indent-line-not-comments 927,38647 (defun coq-indent-region 937,39036 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-smie-lexer.el,862 (defconst coq-smie-dot-friends 20,938 (defun coq-time-indent 23,1015 (defun coq-time-indent-region 29,1156 (defun coq-smie-is-tactic 38,1327 (defun coq-smie-.-deambiguate 48,1560 (defun coq-smie-complete-qualid-backward 77,2277 (defun coq-smie-find-unclosed-match-backward 85,2497 (defun coq-smie-with-deambiguate(95,2825 (defun coq-smie-search-token-forward 113,3390 (defun coq-smie-search-token-backward 156,5197 (defun coq-lonely-:=198,6992 (defun coq-smie-detect-goal-command 215,7753 (defun coq-smie-module-deambiguate 229,8416 (defconst coq-smie-proof-end-tokens248,9312 (defun coq-smie-forward-token 252,9463 (defun coq-is-at-command-real-start(327,12341 (defun coq-smie-:=332,12441 (defun coq-smie-backward-token 368,13890 (defcustom coq-indent-box-style 536,19508 (defconst coq-smie-grammar554,19937 (defun coq-smie-rules 676,24919 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-db486,23272 (defvar coq-commands-db621,33257 (defvar coq-terms-db628,33477 (defun coq-count-match 690,36092 (defun coq-module-opening-p 706,36821 (defun coq-section-command-p 716,37255 (defun coq-goal-command-str-p 720,37352 (defun coq-goal-command-p 746,38677 (defvar coq-keywords-save-strict755,39021 (defvar coq-keywords-save762,39262 (defun coq-save-command-p 767,39341 (defvar coq-keywords-kill-goal778,39669 (defvar coq-keywords-state-changing-misc-commands782,39759 (defvar coq-keywords-goal785,39884 (defvar coq-keywords-decl788,39967 (defvar coq-keywords-defn791,40041 (defvar coq-keywords-state-changing-commands795,40116 (defvar coq-keywords-state-preserving-commands804,40376 (defvar coq-keywords-commands809,40592 (defvar coq-solve-tactics814,40740 (defvar coq-solve-tactics-regexp818,40861 (defvar coq-solve-cheat-tactics822,40995 (defvar coq-solve-cheat-tactics-regexp826,41140 (defvar coq-tacticals830,41298 (defvar coq-reserved836,41437 (defvar coq-reserved-regexp 846,41772 (defvar coq-state-changing-tactics850,41883 (defvar coq-state-preserving-tactics853,41992 (defvar coq-tactics857,42106 (defvar coq-tactics-regexp 860,42195 (defvar coq-retractable-instruct863,42350 (defvar coq-non-retractable-instruct866,42460 (defvar coq-keywords870,42588 (defun proof-regexp-alt-list-symb 876,42812 (defvar coq-keywords-regexp 879,42917 (defvar coq-symbols882,42990 (defvar coq-error-regexp 904,43231 (defvar coq-id 907,43459 (defvar coq-id-shy 908,43484 (defvar coq-ids 911,43577 (defun coq-first-abstr-regexp 913,43643 (defcustom coq-variable-highlight-enable 916,43738 (defvar coq-font-lock-terms922,43865 (defconst coq-save-command-regexp-strict944,44948 (defconst coq-save-command-regexp950,45116 (defconst coq-save-with-hole-regexp955,45269 (defconst coq-goal-command-regexp959,45429 (defconst coq-goal-with-hole-regexp962,45531 (defconst coq-decl-with-hole-regexp966,45665 (defconst coq-defn-with-hole-regexp973,45915 (defconst coq-with-with-hole-regexp983,46205 (defvar coq-font-lock-keywords-1998,46735 (defvar coq-font-lock-keywords 1026,48070 (defun coq-init-syntax-table 1028,48128 (defconst coq-generic-expression1053,48855 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,6737 (defconst coq-control-char-format 258,6862 (defconst coq-control-characters260,6905 (defconst coq-control-region-format-regexp 264,6997 (defconst coq-control-regions266,7080 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,877 (defcustom isabelle-web-page35,1005 (defcustom isa-isabelle-command44,1222 (defvar isabelle-not-found 62,1904 (defun isa-set-isabelle-command 65,2019 (defun isa-shell-command-to-string 88,3037 (defun isa-getenv 94,3261 (defcustom isabelle-program-name-override 114,3960 (defun isa-tool-list-logics 125,4306 (defcustom isabelle-logics-available 132,4552 (defcustom isabelle-chosen-logic 142,4889 (defvar isabelle-chosen-logic-prev 158,5473 (defun isabelle-hack-local-variables-function 161,5593 (defun isabelle-set-prog-name 173,6032 (defun isabelle-choose-logic 197,7152 (defun isa-view-doc 216,7914 (defun isa-tool-list-docs 223,8140 (defconst isabelle-verbatim-regexp 241,8870 (defun isabelle-verbatim 244,9012 (defcustom isabelle-refresh-logics 251,9173 (defvar isabelle-docs-menu259,9501 (defvar isabelle-logics-menu-entries 266,9786 (defun isabelle-logics-menu-calculate 269,9859 (defvar isabelle-time-to-refresh-logics 290,10501 (defun isabelle-logics-menu-refresh 294,10596 (defun isabelle-menu-bar-update-logics 309,11243 (defun isabelle-load-isar-keywords 325,11872 (defun isabelle-create-span-menu 346,12600 (defun isabelle-xml-sml-escapes 362,13031 (defun isabelle-process-pgip 365,13132 isar/isar-autotest.el,31 (defvar isar-long-tests 8,186 isar/isar.el,1595 (defcustom isar-keywords-name 41,939 (defpgdefault completion-table 57,1450 (defcustom isar-web-page59,1503 (defun isar-strip-terminators 73,1853 (defun isar-markup-ml 85,2209 (defun isar-mode-config-set-variables 90,2344 (defun isar-shell-mode-config-set-variables 155,5143 (defun isar-set-proof-find-theorems-command 237,8333 (defpacustom use-find-theorems-form 243,8517 (defun isar-set-undo-commands 248,8683 (defpacustom use-linear-undo 263,9316 (defun isar-configure-from-settings 268,9474 (defun isar-remove-file 276,9624 (defun isar-shell-compute-new-files-list 288,9928 (define-derived-mode isar-shell-mode 307,10498 (define-derived-mode isar-response-mode 312,10625 (define-derived-mode isar-goals-mode 317,10758 (define-derived-mode isar-mode 322,10884 (defpgdefault menu-entries374,12599 (defun isar-set-command 405,13793 (defpgdefault help-menu-entries 410,13923 (defun isar-count-undos 413,13999 (defun isar-find-and-forget 439,14965 (defun isar-goal-command-p 475,16308 (defun isar-global-save-command-p 480,16485 (defvar isar-current-goal 501,17269 (defun isar-state-preserving-p 504,17335 (defvar isar-shell-current-line-width 529,18184 (defun isar-shell-adjust-line-width 534,18376 (defsubst isar-string-wrapping 557,19141 (defsubst isar-positions-of 566,19335 (defcustom isar-wrap-commands-singly 572,19540 (defun isar-command-wrapping 578,19736 (defun isar-preprocessing 586,20050 (defun isar-mode-config 604,20601 (defun isar-shell-mode-config 618,21254 (defun isar-response-mode-config 628,21603 (defun isar-goals-mode-config 638,21938 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,534 (defcustom lego-test-all-name 26,670 (defpgdefault help-menu-entries32,828 (defpgdefault menu-entries36,988 (defvar lego-shell-handle-output47,1289 (defconst lego-process-config55,1587 (defconst lego-pretty-set-width 66,2018 (defconst lego-interrupt-regexp 70,2160 (defcustom lego-www-home-page 75,2277 (defcustom lego-www-latest-release80,2401 (defcustom lego-www-refcard86,2576 (defcustom lego-library-www-page92,2725 (defvar lego-prog-name 101,2941 (defvar lego-shell-cd 104,3010 (defvar lego-shell-proof-completed-regexp 107,3109 (defvar lego-save-command-regexp110,3249 (defvar lego-goal-command-regexp112,3339 (defvar lego-kill-goal-command 115,3430 (defvar lego-forget-id-command 116,3473 (defvar lego-undoable-commands-regexp118,3519 (defvar lego-goal-regexp 127,3893 (defvar lego-outline-regexp129,3938 (defvar lego-outline-heading-end-regexp 135,4113 (defvar lego-shell-outline-regexp 137,4166 (defvar lego-shell-outline-heading-end-regexp 138,4218 (define-derived-mode lego-shell-mode 144,4497 (define-derived-mode lego-mode 151,4658 (define-derived-mode lego-goals-mode 162,4968 (defun lego-count-undos 173,5394 (defun lego-goal-command-p 192,6131 (defun lego-find-and-forget 197,6302 (defun lego-goal-hyp 239,8138 (defun lego-state-preserving-p 248,8335 (defvar lego-shell-current-line-width 264,9038 (defun lego-shell-adjust-line-width 272,9345 (defun lego-mode-config 289,10046 (defun lego-equal-module-filename 357,12097 (defun lego-shell-compute-new-files-list 363,12372 (defun lego-shell-mode-config 373,12755 (defun lego-goals-mode-config 420,14422 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,676 (defcustom hol-light-prog-name 30,877 (defcustom hol-light-use-custom-toplevel 38,1073 (defconst hol-light-pre-sync-cmd52,1569 (defcustom hol-light-init-cmd 56,1743 (defconst hol-light-plain-start-goals-regexp78,2474 (defconst hol-light-annotated-start-goals-regexp 85,2720 (defconst hol-light-plain-interrupt-regexp89,2879 (defconst hol-light-annotated-interrupt-regexp93,3010 (defconst hol-light-plain-prompt-regexp97,3172 (defconst hol-light-annotated-prompt-regexp101,3326 (defconst hol-light-plain-error-regexp105,3498 (defconst hol-light-annotated-error-regexp 116,3823 (defconst hol-light-plain-proof-completed-regexp121,4044 (defconst hol-light-annotated-proof-completed-regexp125,4197 (defconst hol-light-plain-message-start 129,4378 (defconst hol-light-annotated-message-start133,4522 (defconst hol-light-plain-message-end137,4676 (defconst hol-light-annotated-message-end141,4807 (defvar hol-light-keywords 150,4963 (defvar hol-light-rules 151,4995 (defvar hol-light-tactics 152,5024 (defvar hol-light-tacticals 153,5055 (defvar hol-light-update-goal-regexp 365,13121 (defconst hol-light-current-goal-regexp369,13247 (defconst hol-light-additional-subgoal-regexp 375,13441 (defconst hol-light-statenumber-regexp 379,13597 (defconst hol-light-existential-regexp 386,13901 (defconst hol-light-existentials-state-start-regexp 389,14008 (defconst hol-light-existentials-state-end-regexp 392,14155 (defvar proof-shell-delayed-output-start 424,15446 (defvar proof-shell-delayed-output-end 425,15492 (defvar proof-info 426,15536 (defvar proof-action-list 427,15560 (defun proof-shell-action-list-item 428,15591 (defconst hol-light-show-sequent-command 430,15642 (defun hol-light-get-proof-info 432,15710 (defun hol-light-find-begin-of-unfinished-proof 448,16211 (defun hol-light-proof-tree-get-new-subgoals 459,16659 (defpgdefault menu-entries509,18881 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,3371 (defconst hol-light-control-char-format-regexp217,5401 (defconst hol-light-control-char-format 221,5532 (defconst hol-light-control-characters223,5581 (defconst hol-light-control-region-format-regexp 227,5679 (defconst hol-light-control-regions229,5768 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,1562 (defun phox-setup-outline 58,2036 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,1252 (deflocal pg-response-eagerly-raise 32,790 (define-derived-mode proof-response-mode 42,1015 (define-key proof-response-mode-map 69,1970 (define-key proof-response-mode-map 70,2041 (define-key proof-response-mode-map 71,2095 (defun proof-response-config-done 75,2181 (defvar pg-response-special-display-regexp 86,2527 (defconst proof-multiframe-parameters90,2694 (defun proof-multiple-frames-enable 99,2984 (defun proof-three-window-enable 109,3312 (defun proof-select-three-b 112,3375 (defun proof-display-three-b 127,3866 (defvar pg-frame-configuration 138,4256 (defun pg-cache-frame-configuration 142,4403 (defun proof-layout-windows 146,4574 (defun proof-delete-other-frames 186,6361 (defvar pg-response-erase-flag 217,7449 (defun pg-response-maybe-erase221,7578 (defun pg-response-display 265,9041 (defun pg-response-display-with-face 290,9824 (defun pg-response-clear-displays 318,10670 (defun pg-response-message 336,11376 (defun pg-response-warning 342,11611 (defun proof-next-error 357,12017 (defun pg-response-has-error-location 435,14826 (defcustom proof-trace-buffer-max-lines 450,15245 (defun proof-trace-buffer-display 457,15480 (defun proof-trace-buffer-finish 471,15887 (defun pg-thms-buffer-clear 495,16540 generic/pg-user.el,3669 (defvar which-func-modes)28,753 (defun proof-script-new-command-advance 43,1246 (defun proof-maybe-follow-locked-end 67,2171 (defun proof-goto-command-start 93,3007 (defun proof-goto-command-end 116,3954 (defun proof-forward-command 131,4376 (defun proof-backward-command 152,5097 (defun proof-goto-point 163,5311 (defun proof-assert-next-command-interactive 177,5745 (defun proof-assert-until-point-interactive 189,6231 (defun proof-process-buffer 196,6476 (defun proof-undo-last-successful-command 214,6988 (defun proof-undo-and-delete-last-successful-command 219,7150 (defun proof-undo-last-successful-command-1 231,7669 (defun proof-retract-buffer 248,8333 (defun proof-retract-current-goal 263,8941 (defun proof-mouse-goto-point 282,9461 (defvar proof-minibuffer-history 297,9737 (defun proof-minibuffer-cmd 300,9832 (defun proof-frob-locked-end 339,11239 (defmacro proof-if-setting-configured 375,12340 (defmacro proof-define-assistant-command 383,12609 (defmacro proof-define-assistant-command-witharg 396,13064 (defun proof-issue-new-command 416,13886 (defun proof-cd-sync 456,15109 (defun proof-electric-terminator-enable 507,16708 (defun proof-electric-terminator 515,17012 (defun proof-add-completions 543,17982 (defun proof-script-complete 566,18805 (defun pg-copy-span-contents 580,19114 (defun pg-numth-span-higher-or-lower 594,19538 (defun pg-control-span-of 620,20284 (defun pg-move-span-contents 626,20488 (defun pg-fixup-children-spans 677,22606 (defun pg-move-region-down 687,22863 (defun pg-move-region-up 696,23156 (defun pg-pos-for-event 710,23430 (defun pg-span-for-event 716,23651 (defun pg-span-context-menu 720,23795 (defun pg-toggle-visibility 736,24312 (defun pg-create-in-span-context-menu 745,24619 (defun pg-span-undo 770,25647 (defun pg-goals-buffers-hint 783,25885 (defun pg-slow-fontify-tracing-hint 787,26103 (defun pg-response-buffers-hint 791,26292 (defun pg-jump-to-end-hint 803,26707 (defun pg-processing-complete-hint 807,26836 (defun pg-next-error-hint 824,27556 (defun pg-hint 829,27708 (defun pg-identifier-under-mouse-query 840,28057 (defun pg-identifier-near-point-query 851,28381 (defvar proof-query-identifier-history 880,29304 (defun proof-query-identifier 883,29391 (defun pg-identifier-query 894,29747 (defun proof-imenu-enable 927,30895 (defvar pg-input-ring 967,32373 (defvar pg-input-ring-index 970,32430 (defvar pg-stored-incomplete-input 973,32502 (defun pg-previous-input 976,32605 (defun pg-next-input 990,33068 (defun pg-delete-input 995,33190 (defun pg-get-old-input 1008,33528 (defun pg-restore-input 1022,33919 (defun pg-search-start 1033,34209 (defun pg-regexp-arg 1045,34701 (defun pg-search-arg 1057,35149 (defun pg-previous-matching-input-string-position 1071,35566 (defun pg-previous-matching-input 1098,36731 (defun pg-next-matching-input 1117,37581 (defvar pg-matching-input-from-input-string 1125,37964 (defun pg-previous-matching-input-from-input 1129,38078 (defun pg-next-matching-input-from-input 1147,38843 (defun pg-add-to-input-history 1158,39222 (defun pg-remove-from-input-history 1170,39675 (defun pg-clear-input-ring 1181,40055 (define-key proof-mode-map 1198,40525 (define-key proof-mode-map 1199,40585 (defun pg-protected-undo 1201,40657 (defun pg-protected-undo-1 1231,41951 (defun next-undo-elt 1262,43388 (defvar proof-autosend-timer 1289,44344 (deflocal proof-autosend-modified-tick 1291,44405 (defun proof-autosend-enable 1295,44527 (defun proof-autosend-delay 1309,45070 (defun proof-autosend-loop 1313,45203 (defun proof-autosend-loop-all 1327,45763 (defun proof-autosend-loop-next 1351,46543 generic/pg-vars.el,1500 (defvar proof-assistant-cusgrp 22,388 (defvar proof-assistant-internals-cusgrp 28,648 (defvar proof-assistant 34,918 (defvar proof-assistant-symbol 39,1141 (defvar proof-mode-for-shell 52,1683 (defvar proof-mode-for-response 57,1873 (defvar proof-mode-for-goals 62,2099 (defvar proof-mode-for-script 67,2288 (defvar proof-ready-for-assistant-hook 72,2465 (defvar proof-shell-busy 83,2753 (defvar proof-shell-last-queuemode 101,3424 (defvar proof-included-files-list 105,3579 (defvar proof-script-buffer 127,4598 (defvar proof-previous-script-buffer 130,4690 (defvar proof-shell-buffer 134,4863 (defvar proof-goals-buffer 137,4949 (defvar proof-response-buffer 140,5004 (defvar proof-trace-buffer 143,5065 (defvar proof-thms-buffer 147,5219 (defvar proof-shell-error-or-interrupt-seen 151,5374 (defvar pg-response-next-error 156,5598 (defvar proof-shell-proof-completed 159,5705 (defvar proof-shell-silent 173,6090 (defvar proof-shell-last-prompt 176,6178 (defvar proof-shell-last-output 180,6348 (defvar proof-shell-last-output-kind 184,6488 (defvar proof-assistant-settings 204,7252 (defvar pg-tracing-slow-mode 214,7766 (defvar proof-nesting-depth 217,7855 (defvar proof-last-theorem-dependencies 224,8090 (defvar proof-autosend-running 228,8252 (defvar proof-next-command-on-new-line 233,8451 (defcustom proof-general-name 244,8685 (defcustom proof-general-home-page249,8842 (defcustom proof-unnamed-theorem-name255,9002 (defcustom proof-universal-keys261,9186 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,7845 (defgroup prover-config 80,2632 (defcustom proof-guess-command-line 98,3482 (defcustom proof-assistant-home-page 113,3977 (defcustom proof-context-command 119,4147 (defcustom proof-info-command 124,4281 (defcustom proof-showproof-command 131,4552 (defcustom proof-goal-command 136,4688 (defcustom proof-save-command 144,4985 (defcustom proof-find-theorems-command 152,5294 (defcustom proof-query-identifier-command 159,5602 (defcustom proof-assistant-true-value 173,6291 (defcustom proof-assistant-false-value 179,6481 (defcustom proof-assistant-format-int-fn 185,6675 (defcustom proof-assistant-format-float-fn 192,6924 (defcustom proof-assistant-format-string-fn 199,7179 (defcustom proof-assistant-setting-format 206,7446 (defcustom proof-tree-configured 216,7929 (defgroup proof-script 234,8395 (defcustom proof-terminal-string 239,8525 (defcustom proof-electric-terminator-noterminator 249,8913 (defcustom proof-script-sexp-commands 254,9085 (defcustom proof-script-command-end-regexp 265,9544 (defcustom proof-script-command-start-regexp 283,10365 (defcustom proof-script-integral-proofs 294,10828 (defcustom proof-script-fly-past-comments 309,11484 (defcustom proof-script-parse-function 314,11655 (defcustom proof-script-comment-start 332,12300 (defcustom proof-script-comment-start-regexp 343,12737 (defcustom proof-script-comment-end 351,13056 (defcustom proof-script-comment-end-regexp 363,13478 (defcustom proof-string-start-regexp 371,13791 (defcustom proof-string-end-regexp 376,13956 (defcustom proof-case-fold-search 381,14117 (defcustom proof-save-command-regexp 390,14529 (defcustom proof-save-with-hole-regexp 395,14639 (defcustom proof-save-with-hole-result 406,15014 (defcustom proof-goal-command-regexp 416,15458 (defcustom proof-goal-with-hole-regexp 424,15745 (defcustom proof-goal-with-hole-result 436,16188 (defcustom proof-non-undoables-regexp 445,16566 (defcustom proof-nested-undo-regexp 456,17029 (defcustom proof-ignore-for-undo-count 472,17749 (defcustom proof-script-imenu-generic-expression 480,18060 (defcustom proof-goal-command-p 488,18399 (defcustom proof-really-save-command-p 499,18890 (defcustom proof-completed-proof-behaviour 508,19197 (defcustom proof-count-undos-fn 536,20546 (defcustom proof-find-and-forget-fn 548,21097 (defcustom proof-forget-id-command 565,21806 (defcustom pg-topterm-goalhyplit-fn 575,22164 (defcustom proof-kill-goal-command 587,22707 (defcustom proof-undo-n-times-cmd 601,23211 (defcustom proof-nested-goals-history-p 615,23748 (defcustom proof-arbitrary-undo-positions 624,24085 (defcustom proof-state-preserving-p 638,24666 (defcustom proof-activate-scripting-hook 648,25138 (defcustom proof-deactivate-scripting-hook 667,25919 (defcustom proof-no-fully-processed-buffer 676,26249 (defcustom proof-script-evaluate-elisp-comment-regexp 687,26747 (defcustom proof-indent 705,27333 (defcustom proof-indent-hang 710,27440 (defcustom proof-indent-enclose-offset 715,27566 (defcustom proof-indent-open-offset 720,27708 (defcustom proof-indent-close-offset 725,27845 (defcustom proof-indent-any-regexp 730,27983 (defcustom proof-indent-inner-regexp 735,28143 (defcustom proof-indent-enclose-regexp 740,28297 (defcustom proof-indent-open-regexp 745,28451 (defcustom proof-indent-close-regexp 750,28603 (defcustom proof-script-font-lock-keywords 756,28757 (defcustom proof-script-syntax-table-entries 764,29109 (defcustom proof-script-span-context-menu-extensions 782,29505 (defgroup proof-shell 808,30265 (defcustom proof-prog-name 818,30435 (defcustom proof-shell-auto-terminate-commands 830,30902 (defcustom proof-shell-pre-sync-init-cmd 839,31307 (defcustom proof-shell-init-cmd 853,31865 (defcustom proof-shell-init-hook 865,32411 (defcustom proof-shell-restart-cmd 870,32550 (defcustom proof-shell-quit-cmd 875,32705 (defcustom proof-shell-cd-cmd 880,32872 (defcustom proof-shell-start-silent-cmd 897,33543 (defcustom proof-shell-stop-silent-cmd 906,33919 (defcustom proof-shell-silent-threshold 915,34254 (defcustom proof-shell-inform-file-processed-cmd 923,34588 (defcustom proof-shell-inform-file-retracted-cmd 944,35516 (defcustom proof-auto-multiple-files 972,36788 (defcustom proof-cannot-reopen-processed-files 987,37509 (defcustom proof-shell-annotated-prompt-regexp 1007,38300 (defcustom proof-shell-error-regexp 1022,38865 (defcustom proof-shell-truncate-before-error 1042,39675 (defcustom pg-next-error-regexp 1056,40214 (defcustom pg-next-error-filename-regexp 1071,40823 (defcustom pg-next-error-extract-filename 1095,41856 (defcustom proof-shell-interrupt-regexp 1102,42099 (defcustom proof-shell-proof-completed-regexp 1116,42702 (defcustom proof-shell-clear-response-regexp 1129,43218 (defcustom proof-shell-clear-goals-regexp 1141,43678 (defcustom proof-shell-start-goals-regexp 1153,44132 (defcustom proof-shell-end-goals-regexp 1166,44707 (defcustom proof-shell-eager-annotation-start 1180,45297 (defcustom proof-shell-eager-annotation-start-length 1203,46316 (defcustom proof-shell-eager-annotation-end 1214,46742 (defcustom proof-shell-strip-output-markup 1230,47417 (defcustom proof-shell-assumption-regexp 1239,47802 (defcustom proof-shell-process-file 1249,48206 (defcustom proof-shell-retract-files-regexp 1275,49282 (defcustom proof-shell-compute-new-files-list 1288,49770 (defcustom pg-special-char-regexp 1303,50337 (defcustom proof-shell-set-elisp-variable-regexp 1308,50481 (defcustom proof-shell-match-pgip-cmd 1346,52155 (defcustom proof-shell-issue-pgip-cmd 1360,52645 (defcustom proof-use-pgip-askprefs 1365,52818 (defcustom proof-shell-query-dependencies-cmd 1373,53165 (defcustom proof-shell-theorem-dependency-list-regexp 1380,53425 (defcustom proof-shell-theorem-dependency-list-split 1396,54093 (defcustom proof-shell-show-dependency-cmd 1405,54524 (defcustom proof-shell-trace-output-regexp 1427,55430 (defcustom proof-shell-thms-output-regexp 1445,56032 (defcustom proof-shell-interactive-prompt-regexp 1453,56366 (defcustom proof-tokens-activate-command 1472,57019 (defcustom proof-tokens-deactivate-command 1479,57259 (defcustom proof-tokens-extra-modes 1486,57504 (defcustom proof-shell-unicode 1501,58009 (defcustom proof-shell-filename-escapes 1510,58399 (defcustom proof-shell-process-connection-type 1527,59079 (defcustom proof-shell-strip-crs-from-input 1533,59270 (defcustom proof-shell-strip-crs-from-output 1545,59753 (defcustom proof-shell-extend-queue-hook 1553,60121 (defcustom proof-shell-insert-hook 1563,60551 (defcustom proof-script-preprocess 1606,62649 (defcustom proof-shell-handle-delayed-output-hook1612,62800 (defcustom proof-shell-handle-error-or-interrupt-hook1618,63015 (defcustom proof-shell-pre-interrupt-hook1636,63761 (defcustom proof-shell-handle-output-system-specific 1644,64032 (defcustom proof-state-change-hook 1667,65005 (defcustom proof-shell-syntax-table-entries 1677,65398 (defgroup proof-goals 1695,65769 (defcustom pg-subterm-first-special-char 1700,65890 (defcustom pg-subterm-anns-use-stack 1708,66202 (defcustom pg-goals-change-goal 1717,66501 (defcustom pbp-goal-command 1722,66617 (defcustom pbp-hyp-command 1727,66781 (defcustom pg-subterm-help-cmd 1732,66951 (defcustom pg-goals-error-regexp 1739,67195 (defcustom proof-shell-result-start 1744,67363 (defcustom proof-shell-result-end 1750,67605 (defcustom pg-subterm-start-char 1756,67818 (defcustom pg-subterm-sep-char 1767,68292 (defcustom pg-subterm-end-char 1773,68471 (defcustom pg-topterm-regexp 1779,68628 (defcustom proof-goals-font-lock-keywords 1794,69228 (defcustom proof-response-font-lock-keywords 1802,69587 (defcustom proof-shell-font-lock-keywords 1810,69949 (defcustom pg-before-fontify-output-hook 1821,70463 (defcustom pg-after-fontify-output-hook 1829,70824 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,2281 (defface proof-declaration-name-face82,2602 (defface proof-tacticals-name-face91,2888 (defface proof-tactics-name-face100,3150 (defface proof-error-face109,3415 (defface proof-warning-face117,3636 (defface proof-eager-annotation-face126,3893 (defface proof-debug-message-face134,4111 (defface proof-boring-face142,4310 (defface proof-mouse-highlight-face150,4502 (defface proof-command-mouse-highlight-face158,4720 (defface proof-region-mouse-highlight-face166,4959 (defface proof-highlight-dependent-face174,5201 (defface proof-highlight-dependency-face182,5408 (defface proof-active-area-face190,5605 (defface proof-script-sticky-error-face198,5917 (defface proof-script-highlight-error-face206,6146 (defconst proof-face-compat-doc 218,6491 (defconst proof-queue-face 219,6571 (defconst proof-locked-face 220,6639 (defconst proof-declaration-name-face 221,6709 (defconst proof-tacticals-name-face 222,6799 (defconst proof-tactics-name-face 223,6885 (defconst proof-error-face 224,6967 (defconst proof-script-sticky-error-face 225,7035 (defconst proof-script-highlight-error-face 226,7131 (defconst proof-warning-face 227,7233 (defconst proof-eager-annotation-face 228,7305 (defconst proof-debug-message-face 229,7395 (defconst proof-boring-face 230,7479 (defconst proof-mouse-highlight-face 231,7549 (defconst proof-command-mouse-highlight-face 232,7637 (defconst proof-region-mouse-highlight-face 233,7741 (defconst proof-highlight-dependent-face 234,7843 (defconst proof-highlight-dependency-face 235,7939 (defconst proof-active-area-face 236,8037 (defconst proof-script-error-face 237,8117 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,822 (defun proof-display-some-buffers 38,867 (defun proof-menu-define-keys 95,3008 (defun proof-menu-define-main 154,5914 (defvar proof-menu-favourites 163,6099 (defvar proof-menu-settings 166,6206 (defun proof-menu-define-specific 170,6295 (defun proof-assistant-menu-update 213,7557 (defvar proof-help-menu227,7990 (defvar proof-show-hide-menu235,8254 (defvar proof-buffer-menu246,8678 (defun proof-keep-response-history 310,11034 (defconst proof-quick-opts-menu318,11344 (defun proof-quick-opts-vars 540,20411 (defun proof-quick-opts-changed-from-defaults-p 572,21351 (defun proof-quick-opts-changed-from-saved-p 576,21456 (defun proof-set-document-centred 584,21612 (defun proof-set-non-document-centred 597,22038 (defun proof-quick-opts-save 616,22749 (defun proof-quick-opts-reset 621,22917 (defconst proof-config-menu633,23185 (defconst proof-advanced-menu640,23364 (defvar proof-menu658,24048 (defun proof-main-menu 667,24330 (defun proof-aux-menu 679,24669 (defun proof-menu-define-favourites-menu 695,25015 (defun proof-def-favourite 715,25664 (defvar proof-make-favourite-cmd-history 742,26657 (defvar proof-make-favourite-menu-history 745,26742 (defun proof-save-favourites 748,26828 (defun proof-del-favourite 753,26976 (defun proof-read-favourite 770,27532 (defun proof-add-favourite 794,28306 (defun proof-menu-define-settings-menu 821,29351 (defun proof-menu-entry-name 850,30343 (defun proof-menu-entry-for-setting 860,30693 (defun proof-settings-vars 883,31331 (defun proof-settings-changed-from-defaults-p 888,31508 (defun proof-settings-changed-from-saved-p 892,31614 (defun proof-settings-save 896,31717 (defun proof-settings-reset 901,31884 (defun proof-assistant-invisible-command-ifposs 906,32047 (defun proof-maybe-askprefs 928,33017 (defun proof-assistant-settings-cmd 944,33634 (defun proof-assistant-settings-cmds 952,33917 (defvar proof-assistant-format-table967,34359 (defun proof-assistant-format-bool 976,34785 (defun proof-assistant-format-int 979,34898 (defun proof-assistant-format-float 982,34990 (defun proof-assistant-format-string 985,35086 (defun proof-assistant-format 988,35184 generic/proof-mmm.el,70 (defun proof-mmm-set-global 43,1439 (defun proof-mmm-enable 58,1978 generic/proof-script.el,5813 (deflocal proof-active-buffer-fake-minor-mode 46,1418 (deflocal proof-script-buffer-file-name 49,1544 (deflocal pg-script-portions 56,1954 (defalias 'proof-active-buffer-fake-minor-modeproof-active-buffer-fake-minor-mode59,2060 (defun proof-next-element-count 68,2255 (defun proof-element-id 74,2497 (defun proof-next-element-id 78,2666 (deflocal proof-locked-span 114,3970 (deflocal proof-queue-span 121,4236 (deflocal proof-overlay-arrow 130,4722 (defun proof-span-give-warning 136,4849 (defun proof-span-read-only 142,5029 (defun proof-strict-read-only 151,5402 (defsubst proof-set-queue-endpoints 161,5780 (defun proof-set-overlay-arrow 165,5921 (defsubst proof-set-locked-endpoints 176,6259 (defsubst proof-detach-queue 181,6435 (defsubst proof-detach-locked 186,6574 (defsubst proof-set-queue-start 193,6799 (defsubst proof-set-locked-end 197,6925 (defsubst proof-set-queue-end 209,7395 (defun proof-init-segmentation 220,7692 (defun proof-colour-locked 250,8943 (defun proof-colour-locked-span 257,9216 (defun proof-sticky-errors 263,9489 (defun proof-restart-buffers 276,9905 (defun proof-script-buffers-with-spans 300,10838 (defun proof-script-remove-all-spans-and-deactivate 310,11194 (defun proof-script-clear-queue-spans-on-error 314,11384 (defun proof-script-delete-spans 340,12401 (defun proof-script-delete-secondary-spans 345,12600 (defun proof-unprocessed-begin 358,12889 (defun proof-script-end 366,13143 (defun proof-queue-or-locked-end 375,13453 (defun proof-locked-region-full-p 394,14046 (defun proof-locked-region-empty-p 403,14318 (defun proof-only-whitespace-to-locked-region-p 407,14468 (defun proof-in-locked-region-p 417,14817 (defun proof-goto-end-of-locked 429,15074 (defun proof-goto-end-of-locked-if-pos-not-visible-in-window 446,15861 (defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 457,16342 (defun proof-end-of-locked-visible-p 469,16882 (defconst pg-idioms 488,17475 (defconst pg-all-idioms 491,17571 (defun pg-clear-script-portions 495,17692 (defun pg-remove-element 501,17927 (defun pg-get-element 509,18230 (defun pg-add-element 519,18545 (defun pg-invisible-prop 567,20507 (defun pg-set-element-span-invisible 572,20708 (defun pg-toggle-element-span-visibility 585,21274 (defun pg-open-invisible-span 590,21435 (defun pg-make-element-invisible 595,21606 (defun pg-make-element-visible 600,21817 (defun pg-toggle-element-visibility 605,22011 (defun pg-show-all-portions 611,22274 (defun pg-show-all-proofs 633,23018 (defun pg-hide-all-proofs 638,23146 (defun pg-add-proof-element 643,23277 (defun pg-span-name 658,24064 (defvar pg-span-context-menu-keymap691,25271 (defun pg-last-output-displayform 698,25509 (defun pg-set-span-helphighlights 721,26400 (defun proof-complete-buffer-atomic 784,28547 (defun proof-register-possibly-new-processed-file813,29817 (defun proof-query-save-this-buffer-p 859,31691 (defun proof-inform-prover-file-retracted 864,31916 (defun proof-auto-retract-dependencies 884,32767 (defun proof-unregister-buffer-file-name 938,35317 (defsubst proof-action-completed 984,37142 (defun proof-protected-process-or-retract 988,37312 (defun proof-deactivate-scripting-auto 1016,38543 (defun proof-deactivate-scripting-query-user-action 1025,38901 (defun proof-deactivate-scripting-choose-action 1069,40410 (defun proof-deactivate-scripting 1081,40795 (defun proof-activate-scripting 1178,44918 (defun proof-toggle-active-scripting 1278,49457 (defun proof-done-advancing 1317,50702 (defun proof-done-advancing-comment 1385,53199 (defun proof-done-advancing-save 1419,54585 (defun proof-make-goalsave1507,57949 (defun proof-get-name-from-goal 1525,58814 (defun proof-done-advancing-autosave 1545,59839 (defun proof-done-advancing-other 1609,62335 (defun proof-segment-up-to-parser 1638,63299 (defun proof-script-generic-parse-find-comment-end 1708,65580 (defun proof-script-generic-parse-cmdend 1717,65994 (defun proof-script-generic-parse-cmdstart 1768,67890 (defun proof-script-generic-parse-sexp 1807,69490 (defun proof-semis-to-vanillas 1819,69956 (defun proof-next-command-new-line 1872,71629 (defun proof-script-next-command-advance 1877,71835 (defun proof-assert-until-point 1896,72335 (defun proof-assert-electric-terminator 1912,73006 (defun proof-assert-semis 1956,74686 (defun proof-retract-before-change 1970,75447 (defun proof-insert-pbp-command 1993,76103 (defun proof-insert-sendback-command 2008,76606 (defun proof-done-retracting 2034,77509 (defun proof-setup-retract-action 2069,78963 (defun proof-last-goal-or-goalsave 2081,79568 (defun proof-retract-target 2105,80480 (defun proof-retract-until-point-interactive 2184,83733 (defun proof-retract-until-point 2193,84140 (define-derived-mode proof-mode 2248,86145 (defun proof-script-set-visited-file-name 2284,87527 (defun proof-script-set-buffer-hooks 2306,88540 (defun proof-script-kill-buffer-fn 2314,88958 (defun proof-config-done-related 2346,90275 (defun proof-generic-goal-command-p 2417,93132 (defun proof-generic-state-preserving-p 2422,93345 (defun proof-generic-count-undos 2431,93862 (defun proof-generic-find-and-forget 2462,94990 (defconst proof-script-important-settings2513,96762 (defun proof-config-done 2528,97308 (defun proof-setup-parsing-mechanism 2595,99473 (defun proof-setup-imenu 2619,100545 (deflocal proof-segment-up-to-cache 2656,101827 (deflocal proof-segment-up-to-cache-start 2660,101970 (deflocal proof-segment-up-to-cache-end 2661,102015 (deflocal proof-last-edited-low-watermark 2662,102058 (defun proof-segment-up-to-using-cache 2664,102106 (defun proof-segment-cache-contents-for 2692,103226 (defun proof-script-after-change-function 2709,103808 (defun proof-script-set-after-change-functions 2721,104315 generic/proof-shell.el,3766 (defvar proof-marker 35,775 (defvar proof-action-list 38,871 (defsubst proof-shell-invoke-callback 80,2584 (defvar proof-shell-last-goals-output 94,3076 (defvar proof-shell-last-response-output 97,3156 (defvar proof-shell-delayed-output-start 100,3243 (defvar proof-shell-delayed-output-end 104,3425 (defvar proof-shell-delayed-output-flags 108,3605 (defvar proof-shell-interrupt-pending 111,3730 (defvar proof-shell-exit-in-progress 116,3954 (defcustom proof-shell-active-scripting-indicator128,4299 (defun proof-shell-ready-prover 180,5883 (defsubst proof-shell-live-buffer 194,6422 (defun proof-shell-available-p 201,6642 (defun proof-grab-lock 207,6864 (defun proof-release-lock 217,7293 (defcustom proof-shell-fiddle-frames 227,7467 (defun proof-shell-set-text-representation 232,7625 (defun proof-shell-start 240,7953 (defvar proof-shell-kill-function-hooks 416,14054 (defun proof-shell-kill-function 419,14152 (defun proof-shell-clear-state 483,16396 (defun proof-shell-exit 499,16871 (defun proof-shell-bail-out 523,17805 (defun proof-shell-restart 533,18327 (defvar proof-shell-urgent-message-marker 574,19699 (defvar proof-shell-urgent-message-scanner 577,19820 (defun proof-shell-handle-error-output 581,20005 (defun proof-shell-handle-error-or-interrupt 607,20867 (defun proof-shell-error-or-interrupt-action 650,22616 (defun proof-goals-pos 677,23713 (defun proof-pbp-focus-on-first-goal 682,23924 (defsubst proof-shell-string-match-safe 694,24340 (defun proof-shell-handle-immediate-output 698,24501 (defun proof-interrupt-process 765,27108 (defun proof-shell-insert 799,28341 (defun proof-shell-action-list-item 856,30323 (defun proof-shell-set-silent 861,30565 (defun proof-shell-start-silent-item 867,30784 (defun proof-shell-clear-silent 873,30973 (defun proof-shell-stop-silent-item 879,31195 (defsubst proof-shell-should-be-silent 885,31384 (defsubst proof-shell-insert-action-item 897,31957 (defsubst proof-shell-slurp-comments 901,32132 (defun proof-add-to-queue 912,32537 (defun proof-start-queue 964,34489 (defun proof-extend-queue 976,34884 (defun proof-shell-exec-loop 995,35503 (defun proof-shell-insert-loopback-cmd 1077,38443 (defun proof-shell-process-urgent-message 1102,39607 (defun proof-shell-process-urgent-message-default 1158,41632 (defun proof-shell-process-urgent-message-trace 1174,42216 (defun proof-shell-process-urgent-message-retract 1186,42739 (defun proof-shell-process-urgent-message-elisp 1212,43869 (defun proof-shell-process-urgent-message-thmdeps 1227,44364 (defun proof-shell-process-interactive-prompt-regexp 1237,44708 (defun proof-shell-strip-eager-annotations 1249,45064 (defun proof-shell-filter 1265,45564 (defun proof-shell-filter-first-command 1365,48936 (defun proof-shell-process-urgent-messages 1380,49479 (defun proof-shell-filter-manage-output 1430,51045 (defsubst proof-shell-display-output-as-response 1466,52468 (defun proof-shell-handle-delayed-output 1472,52763 (defvar pg-last-tracing-output-time 1576,56335 (defvar pg-last-trace-output-count 1579,56448 (defconst pg-slow-mode-trigger-count 1582,56533 (defconst pg-slow-mode-duration 1585,56638 (defconst pg-fast-tracing-mode-threshold 1588,56720 (defun pg-tracing-tight-loop 1591,56849 (defun pg-finish-tracing-display 1615,57881 (defun proof-shell-wait 1633,58262 (defun proof-done-invisible 1663,59473 (defun proof-shell-invisible-command 1669,59643 (defun proof-shell-invisible-cmd-get-result 1716,61235 (defun proof-shell-invisible-command-invisible-result 1728,61671 (defun pg-insert-last-output-as-comment 1748,62172 (define-derived-mode proof-shell-mode 1767,62644 (defconst proof-shell-important-settings1804,63671 (defun proof-shell-config-done 1810,63786 generic/proof-site.el,708 (defconst proof-assistant-table-default36,1211 (defconst proof-general-short-version78,2412 (defconst proof-general-version-year 84,2599 (defgroup proof-general 91,2752 (defgroup proof-general-internals 96,2860 (defun proof-home-directory-fn 109,3248 (defcustom proof-home-directory120,3620 (defcustom proof-images-directory129,3986 (defcustom proof-info-directory135,4188 (defun proof-add-to-load-path 150,4664 (defcustom proof-assistant-table177,5514 (defcustom proof-assistants 218,6956 (defun proof-ready-for-assistant 247,8110 (defvar proof-general-configured-provers 298,10345 (defun proof-chose-prover 371,12958 (defun proofgeneral 376,13090 (defun proof-visit-example-file 385,13408 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,3010 (defconst proof-splash-welcome 100,3388 (define-derived-mode proof-splash-mode 103,3492 (define-key proof-splash-mode-map 109,3666 (define-key proof-splash-mode-map 110,3718 (defsubst proof-emacs-imagep 115,3845 (defun proof-get-image 120,3970 (defvar proof-splash-timeout-conf 142,4770 (defun proof-splash-centre-spaces 145,4883 (defun proof-splash-remove-screen 172,6039 (defun proof-splash-remove-buffer 189,6695 (defvar proof-splash-seen 200,7083 (defun proof-splash-insert-contents 203,7185 (defun proof-splash-display-screen 243,8315 (defalias 'pg-about pg-about279,9837 (defun proof-splash-message 282,9903 (defun proof-splash-timeout-waiter 295,10361 (defvar proof-splash-old-frame-title-format 308,10921 (defun proof-splash-set-frame-titles 310,10971 (defun proof-splash-unset-frame-titles 319,11286 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,3325 (defgroup proof-tree 90,3804 (defcustom proof-tree-program 95,3945 (defcustom proof-tree-arguments 100,4091 (defgroup proof-tree-internals 110,4251 (defcustom proof-tree-ignored-commands-regexp 118,4520 (defcustom proof-tree-navigation-command-regexp 127,4919 (defcustom proof-tree-cheating-regexp 135,5238 (defcustom proof-tree-current-goal-regexp 144,5635 (defcustom proof-tree-update-goal-regexp 154,6037 (defcustom proof-tree-additional-subgoal-ID-regexp 166,6606 (defcustom proof-tree-existential-regexp 174,6925 (defcustom proof-tree-existentials-state-start-regexp 188,7545 (defcustom proof-tree-existentials-state-end-regexp 199,8096 (defcustom proof-tree-proof-finished-regexp 211,8739 (defcustom proof-tree-get-proof-info 216,8886 (defcustom proof-tree-extract-instantiated-existentials 240,9927 (defcustom proof-tree-show-sequent-command 257,10645 (defcustom proof-tree-find-begin-of-unfinished-proof 271,11267 (defcustom proof-tree-urgent-action-hook 282,11830 (defvar proof-tree-external-display 306,12685 (defvar proof-tree-process 317,13190 (defconst proof-tree-process-name 320,13279 (defconst proof-tree-process-buffer323,13378 (defconst proof-tree-emacs-exec-regexp327,13518 (defvar proof-tree-last-state 331,13685 (defvar proof-tree-current-proof 335,13789 (defvar proof-tree-sequent-hash 340,13970 (defvar proof-tree-existentials-alist 355,14677 (defvar proof-tree-existentials-alist-history 366,15176 (defun proof-tree-stop-external-display 375,15395 (defun proof-tree-insert-output 383,15659 (defun proof-tree-process-filter 394,16042 (defun proof-tree-process-sentinel 420,16740 (defun proof-tree-start-process 428,17066 (defun proof-tree-is-running 457,18249 (defun proof-tree-ensure-running 462,18410 (defconst proof-tree-protocol-version 472,18614 (defun proof-tree-send-message 477,18814 (defun proof-tree-send-configure 491,19300 (defun proof-tree-send-goal-state 500,19586 (defun proof-tree-send-update-sequent 526,20635 (defun proof-tree-send-switch-goal 539,21072 (defun proof-tree-send-proof-finished 548,21398 (defun proof-tree-send-proof-complete 562,21910 (defun proof-tree-send-undo 570,22159 (defun proof-tree-send-quit-proof 575,22341 (defun proof-tree-record-existentials-state 586,22676 (defun proof-tree-undo-state-var 599,23226 (defun proof-tree-undo-existentials 618,24007 (defun proof-tree-delete-existential-assoc 626,24322 (defun proof-tree-add-existential-assoc 632,24585 (defun proof-tree-clear-existentials 645,25200 (defun proof-tree-show-goal-callback 655,25468 (defun proof-tree-make-show-goal-callback 676,26455 (defun proof-tree-urgent-action 680,26616 (defun proof-tree-quit-proof 745,29152 (defun proof-tree-register-existentials 755,29571 (defun proof-tree-extract-goals 768,30115 (defun proof-tree-extract-list 790,31060 (defun proof-tree-extract-existential-info 813,32030 (defun proof-tree-handle-proof-progress 833,32901 (defun proof-tree-handle-navigation 884,34937 (defun proof-tree-handle-proof-command 902,35663 (defun proof-tree-handle-undo 917,36325 (defun proof-tree-update-sequent 949,37624 (defun proof-tree-handle-delayed-output 990,39392 (defun proof-tree-leave-buffer 1043,41504 (defun proof-tree-display-current-proof 1055,41787 (defun proof-tree-external-display-toggle 1087,43128 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,1619 (defgroup proof-user-options 21,564 (defun proof-set-value 29,743 (defcustom proof-electric-terminator-enable 62,1866 (defcustom proof-toolbar-enable 74,2398 (defcustom proof-imenu-enable 80,2571 (defcustom pg-show-hints 86,2742 (defcustom proof-shell-quiet-errors 91,2875 (defcustom proof-trace-output-slow-catchup 98,3146 (defcustom proof-strict-state-preserving 108,3643 (defcustom proof-strict-read-only 121,4252 (defcustom proof-three-window-enable 134,4831 (defcustom proof-multiple-frames-enable 153,5581 (defcustom proof-delete-empty-windows 162,5914 (defcustom proof-shrink-windows-tofit 173,6445 (defcustom proof-auto-raise-buffers 180,6717 (defcustom proof-colour-locked 187,6952 (defcustom proof-sticky-errors 195,7202 (defcustom proof-query-file-save-when-activating-scripting202,7419 (defcustom proof-prog-name-ask218,8139 (defcustom proof-prog-name-guess224,8299 (defcustom proof-tidy-response232,8564 (defcustom proof-keep-response-history246,9027 (defcustom pg-input-ring-size 256,9415 (defcustom proof-general-debug 261,9567 (defcustom proof-use-parser-cache 270,9938 (defcustom proof-follow-mode 277,10192 (defcustom proof-auto-action-when-deactivating-scripting 301,11369 (defcustom proof-rsh-command 329,12551 (defcustom proof-disappearing-proofs 345,13109 (defcustom proof-full-annotation 350,13270 (defcustom proof-output-tooltips 360,13733 (defcustom proof-minibuffer-messages 371,14240 (defcustom proof-autosend-enable 379,14549 (defcustom proof-autosend-delay 385,14729 (defcustom proof-autosend-all 391,14887 (defcustom proof-fast-process-buffer 396,15056 generic/proof-utils.el,1645 (defmacro proof-with-current-buffer-if-exists 61,1735 (defmacro proof-with-script-buffer 70,2112 (defmacro proof-map-buffers 81,2493 (defmacro proof-sym 86,2678 (defsubst proof-try-require 91,2839 (defun proof-save-some-buffers 104,3170 (defun proof-save-this-buffer 124,3766 (defun proof-file-truename 137,4130 (defun proof-files-to-buffers 141,4312 (defun proof-buffers-in-mode 149,4551 (defun pg-save-from-death 163,5001 (defun proof-define-keys 182,5617 (defun pg-remove-specials 193,5902 (defun pg-remove-specials-in-string 203,6238 (defun proof-safe-split-window-vertically 213,6463 (defun proof-warn-if-unset 218,6643 (defun proof-get-window-for-buffer 223,6861 (defun proof-display-and-keep-buffer 272,9171 (defun proof-clean-buffer 314,10894 (defun pg-internal-warning 330,11550 (defun proof-debug 338,11832 (defun proof-switch-to-buffer 353,12383 (defun proof-resize-window-tofit 375,13507 (defun proof-submit-bug-report 470,17355 (defun proof-deftoggle-fn 505,18712 (defmacro proof-deftoggle 520,19378 (defun proof-defintset-fn 531,19891 (defmacro proof-defintset 550,20715 (defun proof-deffloatset-fn 557,21094 (defmacro proof-deffloatset 573,21808 (defun proof-defstringset-fn 580,22193 (defmacro proof-defstringset 593,22819 (defun proof-escape-keymap-doc 606,23275 (defmacro proof-defshortcut 610,23429 (defmacro proof-definvisible 625,24027 (defun pg-custom-save-vars 652,24956 (defun pg-custom-reset-vars 668,25600 (defun proof-locate-executable 681,25937 (defun pg-current-word-pos 696,26487 (defsubst proof-shell-strip-output-markup 741,28142 (defun proof-minibuffer-message 747,28406 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,1121 (defvar holes-active-hole 50,1299 (defgroup holes 60,1496 (defcustom holes-empty-hole-string 65,1595 (defcustom holes-empty-hole-regexp 70,1738 (defface active-hole-face92,2440 (defface inactive-hole-face102,2856 (defvar hole-map116,3297 (defvar holes-mode-map126,3688 (defun holes-region-beginning-or-nil 172,5425 (defun holes-region-end-or-nil 176,5561 (defun holes-copy-active-region 180,5679 (defun holes-is-hole-p 186,5889 (defun holes-hole-start-position 190,5981 (defun holes-hole-end-position 196,6164 (defun holes-hole-buffer 201,6335 (defun holes-hole-at 207,6509 (defun holes-active-hole-exist-p 212,6679 (defun holes-active-hole-start-position 219,6932 (defun holes-active-hole-end-position 227,7300 (defun holes-active-hole-buffer 236,7663 (defun holes-goto-active-hole 244,7964 (defun holes-highlight-hole-as-active 253,8223 (defun holes-highlight-hole 261,8531 (defun holes-disable-active-hole 269,8818 (defun holes-set-active-hole 282,9350 (defun holes-is-in-hole-p 292,9695 (defun holes-make-hole 296,9833 (defun holes-make-hole-at 314,10489 (defun holes-clear-hole 328,10942 (defun holes-clear-hole-at 337,11200 (defun holes-map-holes 345,11456 (defun holes-clear-all-buffer-holes 349,11610 (defun holes-next 359,11911 (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,16167 (defsubst holes-track-mouse-clicks 478,16225 (defun holes-mouse-replace-active-hole 482,16335 (defun holes-destroy-hole 496,16806 (defsubst holes-hole-at-event 510,17188 (defun holes-mouse-destroy-hole 514,17288 (defun holes-mouse-forget-hole 521,17509 (defun holes-mouse-set-make-active-hole 531,17801 (defun holes-mouse-set-active-hole 547,18300 (defun holes-set-point-next-hole-destroy 556,18551 (defun holes-replace-string-by-holes-backward 582,19532 (defun holes-skeleton-end-hook 600,20232 (defconst holes-jump-doc609,20670 (defun holes-replace-string-by-holes-backward-jump 616,20876 (define-minor-mode holes-mode 633,21558 (defun holes-abbrev-complete 728,25040 (defun holes-insert-and-expand 738,25383 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,2317 (defvar maths-menu-tokenise-insert 59,2426 (defun maths-menu-build-menu 62,2563 (defvar maths-menu-menu84,3324 (defvar maths-menu-mode-map344,12882 (define-minor-mode maths-menu-mode352,13101 lib/pg-dev.el,199 (defconst pg-dev-lisp-font-lock-keywords58,1666 (defun pg-loadpath 84,2365 (defun unload-pg 94,2536 (defun profile-pg 125,3430 (defun elp-pack-number 155,4537 (defun pg-bug-references 164,4737 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,160 (defvar proof-running-on-win32 32,975 (defun pg-custom-undeclare-variable 53,1777 (defmacro save-selected-frame 86,2602 (defmacro declare-function 152,4610 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,3027 (defun texi-docstring-magic-splice-sep 93,3192 (defconst texi-docstring-magic-munge-table103,3497 (defun texi-docstring-magic-untabify 193,7260 (defun texi-docstring-magic-munge-docstring 200,7458 (defun texi-docstring-magic-texi 239,8739 (defun texi-docstring-magic-format-default 252,9179 (defun texi-docstring-magic-texi-for 268,9812 (defconst texi-docstring-magic-comment326,11771 (defun texi-docstring-magic 332,11925 (defun texi-docstring-magic-face-at-point 366,13004 (defun texi-docstring-magic-insert-magic 381,13527 lib/unicode-chars.el,80 (defvar unicode-chars-alist12,348 (defun unicode-chars-list-chars 5051,245975 lib/unicode-tokens.el,5901 (defgroup unicode-tokens-options 55,1711 (defcustom unicode-tokens-add-help-echo 60,1836 (defun unicode-tokens-toggle-add-help-echo 65,2003 (defvar unicode-tokens-token-symbol-map 79,2409 (defvar unicode-tokens-token-format 98,3068 (defvar unicode-tokens-token-variant-format-regexp 104,3317 (defvar unicode-tokens-shortcut-alist 118,3850 (defvar unicode-tokens-shortcut-replacement-alist 124,4127 (defvar unicode-tokens-control-region-format-regexp 132,4333 (defvar unicode-tokens-control-char-format-regexp 139,4701 (defvar unicode-tokens-control-regions 146,5062 (defvar unicode-tokens-control-characters 149,5138 (defvar unicode-tokens-control-char-format 152,5220 (defvar unicode-tokens-control-region-format-start 155,5333 (defvar unicode-tokens-control-region-format-end 158,5450 (defvar unicode-tokens-tokens-customizable-variables 161,5563 (defconst unicode-tokens-configuration-variables168,5731 (defun unicode-tokens-config 183,6130 (defun unicode-tokens-config-var 187,6275 (defun unicode-tokens-copy-configuration-variables 199,6715 (defvar unicode-tokens-token-list 227,7931 (defvar unicode-tokens-hash-table 230,8051 (defvar unicode-tokens-token-match-regexp 233,8167 (defvar unicode-tokens-uchar-hash-table 239,8450 (defvar unicode-tokens-uchar-regexp 243,8637 (defgroup unicode-tokens-faces 251,8822 (defconst unicode-tokens-font-family-alternatives261,9124 (defface unicode-tokens-symbol-font-face276,9643 (defface unicode-tokens-script-font-face287,10116 (defface unicode-tokens-fraktur-font-face292,10260 (defface unicode-tokens-serif-font-face297,10385 (defface unicode-tokens-sans-font-face302,10522 (defface unicode-tokens-highlight-face307,10644 (defconst unicode-tokens-fonts316,11006 (defconst unicode-tokens-fontsymb-properties325,11223 (define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map353,12844 (define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist371,13396 (defconst unicode-tokens-font-lock-extra-managed-props384,13727 (defun unicode-tokens-font-lock-keywords 388,13881 (defun unicode-tokens-calculate-token-match 421,15252 (defun unicode-tokens-usable-composition 451,16288 (defun unicode-tokens-help-echo 464,16667 (defvar unicode-tokens-show-symbols 469,16869 (defun unicode-tokens-interpret-composition 472,16983 (defun unicode-tokens-font-lock-compose-symbol 490,17495 (defun unicode-tokens-prepend-text-properties-in-match 528,19027 (defun unicode-tokens-prepend-text-property 542,19605 (defun unicode-tokens-show-symbols 567,20750 (defun unicode-tokens-symbs-to-props 575,21060 (defvar unicode-tokens-show-controls 595,21759 (defun unicode-tokens-show-controls 598,21850 (defun unicode-tokens-control-char 610,22363 (defun unicode-tokens-control-region 619,22802 (defun unicode-tokens-control-font-lock-keywords 630,23349 (defvar unicode-tokens-use-shortcuts 641,23673 (defun unicode-tokens-use-shortcuts 644,23776 (defun unicode-tokens-map-ordering 660,24372 (defun unicode-tokens-quail-define-rules 669,24725 (defun unicode-tokens-insert-token 692,25402 (defun unicode-tokens-annotate-region 701,25706 (defun unicode-tokens-insert-control 725,26544 (defun unicode-tokens-insert-uchar-as-token 735,26993 (defun unicode-tokens-delete-token-near-point 741,27214 (defun unicode-tokens-delete-backward-char 753,27655 (defun unicode-tokens-delete-char 764,28036 (defun unicode-tokens-delete-backward-1 775,28390 (defun unicode-tokens-delete-1 792,28986 (defun unicode-tokens-prev-token 808,29530 (defun unicode-tokens-rotate-token-forward 816,29827 (defun unicode-tokens-rotate-token-backward 843,30717 (defun unicode-tokens-replace-shortcut-match 848,30919 (defun unicode-tokens-replace-shortcuts 857,31289 (defun unicode-tokens-replace-unicode-match 871,31887 (defun unicode-tokens-replace-unicode 878,32188 (defun unicode-tokens-copy-token 895,32787 (define-button-type 'unicode-tokens-listunicode-tokens-list902,33008 (defun unicode-tokens-list-tokens 908,33212 (defun unicode-tokens-list-shortcuts 947,34396 (defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars965,35034 (defun unicode-tokens-encode-in-temp-buffer 967,35107 (defun unicode-tokens-encode 985,35763 (defun unicode-tokens-encode-str 991,35999 (defun unicode-tokens-copy 995,36161 (defun unicode-tokens-paste 1004,36567 (defvar unicode-tokens-highlight-unicode 1023,37288 (defconst unicode-tokens-unicode-highlight-patterns1026,37380 (defun unicode-tokens-highlight-unicode 1030,37549 (defun unicode-tokens-highlight-unicode-setkeywords 1042,38012 (defun unicode-tokens-initialise 1054,38381 (defvar unicode-tokens-mode-map 1074,39052 (defvar unicode-tokens-display-table1077,39149 (define-minor-mode unicode-tokens-mode1084,39400 (defun unicode-tokens-set-font-var 1220,43975 (defun unicode-tokens-set-font-var-aux 1236,44464 (defun unicode-tokens-mouse-set-font 1267,45625 (defsubst unicode-tokens-face-font-sym 1280,46139 (defun unicode-tokens-set-font-restart 1284,46319 (defun unicode-tokens-save-fonts 1295,46629 (defun unicode-tokens-custom-save-faces 1303,46885 (define-key unicode-tokens-mode-map1320,47341 (define-key unicode-tokens-mode-map1323,47448 (defvar unicode-tokens-quail-translation-keymap1331,47707 (define-key unicode-tokens-quail-translation-keymap1338,47897 (defun unicode-tokens-quail-delete-last-char 1342,48031 (define-key unicode-tokens-mode-map 1357,48458 (define-key unicode-tokens-mode-map 1359,48550 (define-key unicode-tokens-mode-map1361,48641 (define-key unicode-tokens-mode-map1363,48747 (define-key unicode-tokens-mode-map1366,48862 (define-key unicode-tokens-mode-map1368,48971 (define-key unicode-tokens-mode-map1370,49079 (define-key unicode-tokens-mode-map1372,49185 (defun unicode-tokens-customize-submenu 1380,49309 (defun unicode-tokens-define-menu 1387,49532 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,7116 @node Top145,4238 @node Preface184,5437 @node News for Version 4.2News for Version 4.2209,6076 @node News for Version 4.1News for Version 4.1222,6532 @node News for Version 4.0News for Version 4.0233,6839 @node Future254,7690 @node Credits283,9025 @node Introducing Proof GeneralIntroducing Proof General405,13134 @node Installing Proof GeneralInstalling Proof General460,15108 @node Quick start guideQuick start guide474,15557 @node Features of Proof GeneralFeatures of Proof General519,17751 @node Supported proof assistantsSupported proof assistants625,22295 @node Prerequisites for this manualPrerequisites for this manual677,24285 @node Organization of this manualOrganization of this manual721,25904 @node Basic Script ManagementBasic Script Management747,26732 @node Walkthrough example in IsabelleWalkthrough example in Isabelle766,27332 @node Proof scriptsProof scripts1051,38727 @node Script buffersScript buffers1094,40847 @node Locked queue and editing regionsLocked queue and editing regions1116,41424 @node Goal-save sequencesGoal-save sequences1172,43571 @node Active scripting bufferActive scripting buffer1209,45055 @node Summary of Proof General buffersSummary of Proof General buffers1282,48688 @node Script editing commandsScript editing commands1331,50945 @node Script processing commandsScript processing commands1411,53904 @node Proof assistant commandsProof assistant commands1540,59334 @node Toolbar commandsToolbar commands1733,66262 @node Interrupting during trace outputInterrupting during trace output1758,67221 @node Advanced Script Management and EditingAdvanced Script Management and Editing1798,69151 @node Document centred workingDocument centred working1819,69772 @node Automatic processingAutomatic processing1931,74450 @node Visibility of completed proofsVisibility of completed proofs1986,76498 @node Switching between proof scriptsSwitching between proof scripts2041,78438 @node View of processed files View of processed files 2078,80410 @node Retracting across filesRetracting across files2138,83461 @node Asserting across filesAsserting across files2151,84092 @node Automatic multiple file handlingAutomatic multiple file handling2164,84658 @node Escaping script managementEscaping script management2189,85692 @node Editing featuresEditing features2246,87804 @node Unicode symbols and special layout supportUnicode symbols and special layout support2316,90583 @node Maths menuMaths menu2358,92141 @node Unicode Tokens modeUnicode Tokens mode2375,92832 @node Configuring tokens symbols and shortcutsConfiguring tokens symbols and shortcuts2425,95255 @node Special layout Special layout 2455,96216 @node Moving between Unicode and tokensMoving between Unicode and tokens2565,100334 @node Finding available tokens shortcuts and symbolsFinding available tokens shortcuts and symbols2620,102445 @node Selecting suitable fontsSelecting suitable fonts2659,103619 @node Support for other PackagesSupport for other Packages2724,106607 @node Syntax highlightingSyntax highlighting2754,107443 @node Imenu and SpeedbarImenu and Speedbar2782,108446 @node Support for outline modeSupport for outline mode2828,110117 @node Support for completionSupport for completion2853,111246 @node Support for tagsSupport for tags2910,113408 @node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing2962,115756 @node Goals buffer commandsGoals buffer commands2978,116351 @node Graphical Proof-Tree VisualizationGraphical Proof-Tree Visualization3077,120504 @node Starting and Stopping Proof-Tree VisualizationStarting and Stopping Proof-Tree Visualization3100,121396 @node Features of ProoftreeFeatures of Prooftree3128,122553 @node Prooftree CustomizationProoftree Customization3160,123764 @node Customizing Proof GeneralCustomizing Proof General3184,124643 @node Basic optionsBasic options3224,126313 @node How to customizeHow to customize3248,127083 @node Display customizationDisplay customization3295,129050 @node User optionsUser options3463,136012 @node Changing facesChanging faces3699,144680 @node Script buffer facesScript buffer faces3721,145555 @node Goals and response facesGoals and response faces3767,147155 @node Tweaking configuration settingsTweaking configuration settings3812,148687 @node Hints and TipsHints and Tips3869,151213 @node Adding your own keybindingsAdding your own keybindings3888,151814 @node Using file variablesUsing file variables3952,154428 @node Using abbreviationsUsing abbreviations4029,157156 @node LEGO Proof GeneralLEGO Proof General4068,158571 @node LEGO specific commandsLEGO specific commands4109,159940 @node LEGO tagsLEGO tags4129,160395 @node LEGO customizationsLEGO customizations4139,160642 @node Coq Proof GeneralCoq Proof General4169,161482 @node Coq-specific commandsCoq-specific commands4185,161848 @node Multiple File SupportMultiple File Support4208,162356 @node Automatic Compilation in DetailAutomatic Compilation in Detail4278,164945 @node Locking AncestorsLocking Ancestors4353,168296 @node Customizing Coq Multiple File SupportCustomizing Coq Multiple File Support4386,169721 @node Current LimitationsCurrent Limitations4615,179328 @node Editing multiple proofsEditing multiple proofs4641,180180 @node User-loaded tacticsUser-loaded tactics4665,181288 @node Holes featureHoles feature4729,183762 @node Proof-Tree VisualizationProof-Tree Visualization4754,184981 @node Isabelle Proof GeneralIsabelle Proof General4766,185331 @node Choosing logic and starting isabelleChoosing logic and starting isabelle4792,186207 @node Isabelle commandsIsabelle commands4861,189008 @node Isabelle settingsIsabelle settings5004,193200 @node Isabelle customizationsIsabelle customizations5018,193782 @node HOL Light Proof GeneralHOL Light Proof General5041,194275 @node Shell Proof GeneralShell Proof General5088,196254 @node Obtaining and InstallingObtaining and Installing5124,197713 @node Obtaining Proof GeneralObtaining Proof General5139,198078 @node Installing Proof General from tarballInstalling Proof General from tarball5165,198960 @node Setting the names of binariesSetting the names of binaries5189,199750 @node Notes for syssiesNotes for syssies5217,200690 @node Bugs and EnhancementsBugs and Enhancements5293,203687 @node References5314,204502 @node History of Proof GeneralHistory of Proof General5354,205525 @node Old News for 3.0Old News for 3.05448,209690 @node Old News for 3.1Old News for 3.15518,213384 @node Old News for 3.2Old News for 3.25544,214556 @node Old News for 3.3Old News for 3.35605,217559 @node Old News for 3.4Old News for 3.45624,218456 @node Old News for 3.5Old News for 3.55646,219511 @node Old News for 3.6Old News for 3.65650,219568 @node Old News for 3.7Old News for 3.75655,219668 @node Function IndexFunction Index5685,221122 @node Variable IndexVariable Index5689,221198 @node Keystroke IndexKeystroke Index5693,221278 @node Concept IndexConcept Index5697,221344 doc/PG-adapting.texi,4541 @node Top137,3999 @node Introduction175,5149 @node Future216,6802 @node Credits252,8398 @node Beginning with a New ProverBeginning with a New Prover262,8690 @node Overview of adding a new proverOverview of adding a new prover302,10632 @node Demonstration instance and easy configurationDemonstration instance and easy configuration384,14281 @node Major modes used by Proof GeneralMajor modes used by Proof General453,17672 @node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands496,19382 @node Settings for generic user-level commandsSettings for generic user-level commands511,19928 @node Menu configurationMenu configuration556,21660 @node Toolbar configurationToolbar configuration580,22577 @node Proof Script SettingsProof Script Settings639,24814 @node Recognizing commands and commentsRecognizing commands and comments662,25426 @node Recognizing proofsRecognizing proofs799,31879 @node Recognizing other elementsRecognizing other elements903,36183 @node Configuring undo behaviourConfiguring undo behaviour966,38662 @node Nested proofsNested proofs1103,44049 @node Safe (state-preserving) commandsSafe (state-preserving) commands1143,45675 @node Activate scripting hookActivate scripting hook1166,46628 @node Automatic multiple filesAutomatic multiple files1190,47498 @node Completely asserted buffersCompletely asserted buffers1211,48344 @node Completions1244,49809 @node Proof Shell SettingsProof Shell Settings1285,51299 @node Proof shell commandsProof shell commands1316,52581 @node Script input to the shellScript input to the shell1493,60345 @node Settings for matching various output from proof processSettings for matching various output from proof process1563,63549 @node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1690,69105 @node Hooks and other settingsHooks and other settings1950,80395 @node Goals Buffer SettingsGoals Buffer Settings2029,83539 @node Splash Screen SettingsSplash Screen Settings2103,86529 @node Global ConstantsGlobal Constants2129,87284 @node Handling Multiple FilesHandling Multiple Files2155,88113 @node Configuring Editing SyntaxConfiguring Editing Syntax2324,96782 @node Configuring Font LockConfiguring Font Lock2381,98899 @node Configuring TokensConfiguring Tokens2457,102611 @node Configuring Proof-Tree VisualizationConfiguring Proof-Tree Visualization2507,104731 @node Prerequisites2524,105271 @node Proof-Tree Display InternalsProof-Tree Display Internals2587,107922 @node Organization of the CodeOrganization of the Code2605,108412 @node Communication2701,112675 @node Guards2726,113787 @node Urgent and Delayed ActionsUrgent and Delayed Actions2780,115932 @node Full AnnotationFull Annotation2841,118440 @node Configuring Prooftree for a New Proof AssistantConfiguring Prooftree for a New Proof Assistant2855,119014 @node Proof Tree Elisp configurationProof Tree Elisp configuration2867,119346 @node Prooftree AdaptionProoftree Adaption2888,120176 @node Writing More Lisp CodeWriting More Lisp Code2908,120855 @node Default values for generic settingsDefault values for generic settings2925,121500 @node Adding prover-specific configurationsAdding prover-specific configurations2955,122583 @node Useful variablesUseful variables2998,123865 @node Useful functions and macrosUseful functions and macros3013,124364 @node Internals of Proof GeneralInternals of Proof General3123,128676 @node Spans3153,129606 @node Proof General site configurationProof General site configuration3168,129979 @node Configuration variable mechanismsConfiguration variable mechanisms3251,133115 @node Global variablesGlobal variables3381,138831 @node Proof script modeProof script mode3456,141455 @node Proof shell modeProof shell mode3720,153412 @node Debugging4277,176003 @node Plans and IdeasPlans and Ideas4320,176879 @node Proof by pointing and similar featuresProof by pointing and similar features4341,177601 @node Granularity of atomic command sequencesGranularity of atomic command sequences4379,179259 @node Browser mode for script files and theoriesBrowser mode for script files and theories4424,181484 @node Demonstration InstantiationsDemonstration Instantiations4454,182515 @node demoisa-easy.el4470,182946 @node demoisa.el4532,185139 @node Function IndexFunction Index4686,190060 @node Variable IndexVariable Index4690,190136 @node Concept IndexConcept Index4699,190315 generic/proofgeneral-pkg.el,0 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