acl2/acl2.el,0 acl2/x-symbol-acl2.el,0 coq/coq-abbrev.el,152 (defun holes-show-doc holes-show-doc4,90 (defpgdefault menu-entriesmenu-entries151,7985 (defpgdefault help-menu-entrieshelp-menu-entries349,19008 coq/coq-autotest.el,0 coq/coq.el,6716 (defun proofstack proofstack23,436 (defun proofstack proofstack24,508 (defun proofstack proofstack25,580 (defcustom coq-prog-name coq-prog-name28,670 (defcustom coq-compile-file-command coq-compile-file-command33,779 (defcustom coq-default-undo-limit coq-default-undo-limit43,1148 (defconst coq-shell-init-cmd coq-shell-init-cmd48,1276 (defconst coq-shell-restart-cmd coq-shell-restart-cmd58,1535 (defvar coq-shell-prompt-pattern coq-shell-prompt-pattern66,1836 (defvar coq-shell-cd coq-shell-cd73,2112 (defvar coq-shell-abort-goal-regexp coq-shell-abort-goal-regexp77,2267 (defvar coq-shell-proof-completed-regexp coq-shell-proof-completed-regexp80,2393 (defvar coq-goal-regexpcoq-goal-regexp83,2524 (defun coq-library-directory coq-library-directory92,2713 (defcustom coq-tags coq-tags99,2893 (defconst coq-interrupt-regexp coq-interrupt-regexp104,3043 (defcustom coq-www-home-page coq-www-home-page109,3164 (defun coq-insert-section coq-insert-section119,3351 (defconst module-kinds-table module-kinds-table128,3591 (defconst modtype-kinds-tablemodtype-kinds-table132,3727 (defun coq-insert-module coq-insert-module136,3856 (defvar coq-outline-regexpcoq-outline-regexp156,4534 (defvar coq-outline-heading-end-regexp coq-outline-heading-end-regexp161,4943 (defvar coq-shell-outline-regexp coq-shell-outline-regexp163,5002 (defvar coq-shell-outline-heading-end-regexp coq-shell-outline-heading-end-regexp164,5052 (defconst coq-kill-goal-command coq-kill-goal-command169,5162 (defconst coq-forget-id-command coq-forget-id-command170,5205 (defconst coq-back-n-command coq-back-n-command171,5251 (defconst coq-state-preserving-tactics-regexp coq-state-preserving-tactics-regexp174,5295 (defconst coq-state-changing-commands-regexpcoq-state-changing-commands-regexp176,5396 (defconst coq-state-preserving-commands-regexp coq-state-preserving-commands-regexp178,5503 (defconst coq-commands-regexp coq-commands-regexp180,5615 (defvar coq-retractable-instruct-regexp coq-retractable-instruct-regexp182,5693 (defvar coq-keywords-sectioncoq-keywords-section185,5785 (defvar coq-section-regexp coq-section-regexp188,5878 (defun coq-set-undo-limit coq-set-undo-limit222,6977 (defconst coq-keywords-decl-defn-regexpcoq-keywords-decl-defn-regexp233,7415 (defun coq-proof-mode-p coq-proof-mode-p237,7565 (defun coq-is-comment-or-proverprocp coq-is-comment-or-proverprocp248,7975 (defun coq-is-goalsave-p coq-is-goalsave-p250,8079 (defun coq-is-module-equal-p coq-is-module-equal-p251,8154 (defun coq-is-def-p coq-is-def-p254,8350 (defun coq-is-decl-defn-p coq-is-decl-defn-p256,8458 (defun coq-state-preserving-command-p coq-state-preserving-command-p261,8625 (defun coq-command-p coq-command-p264,8759 (defun coq-state-preserving-tactic-p coq-state-preserving-tactic-p267,8859 (defun coq-state-changing-tactic-p coq-state-changing-tactic-p272,9007 (defun coq-state-changing-command-p coq-state-changing-command-p279,9241 (defun coq-section-or-module-start-p coq-section-or-module-start-p285,9549 (defun build-list-id-from-string build-list-id-from-string294,9790 (defun coq-last-prompt-info coq-last-prompt-info307,10320 (defun coq-last-prompt-info-safe coq-last-prompt-info-safe324,10937 (defvar coq-last-but-one-statenum coq-last-but-one-statenum334,11452 (defvar coq-last-but-one-proofnum coq-last-but-one-proofnum336,11519 (defvar coq-last-but-one-proofstack coq-last-but-one-proofstack338,11582 (defun coq-get-span-statenum coq-get-span-statenum340,11624 (defun coq-get-span-proofnum coq-get-span-proofnum345,11739 (defun coq-get-span-proofstack coq-get-span-proofstack350,11854 (defun coq-set-span-statenum coq-set-span-statenum355,11998 (defun coq-set-span-proofnum coq-set-span-proofnum360,12129 (defun coq-set-span-proofstack coq-set-span-proofstack365,12260 (defun proof-last-locked-span proof-last-locked-span370,12420 (defun coq-set-state-infos coq-set-state-infos385,13024 (defun count-not-intersection count-not-intersection416,14627 (defun coq-find-and-forget-v81 coq-find-and-forget-v81447,15881 (defun coq-find-and-forget-v80 coq-find-and-forget-v80471,16748 (defun coq-find-and-forget coq-find-and-forget566,21443 (defvar coq-current-goal coq-current-goal578,21897 (defun coq-goal-hyp coq-goal-hyp581,21962 (defun coq-state-preserving-p coq-state-preserving-p595,22425 (defun coq-SearchIsos coq-SearchIsos602,22742 (defun coq-guess-or-ask-for-string coq-guess-or-ask-for-string612,23094 (defun coq-ask-do coq-ask-do622,23415 (defun coq-Print coq-Print631,23676 (defun coq-About coq-About635,23800 (defun coq-Print-implicit coq-Print-implicit639,23919 (defun coq-Check coq-Check644,24072 (defun coq-Show coq-Show649,24182 (defun coq-PrintHint coq-PrintHint664,24619 (defun coq-end-Section coq-end-Section670,24763 (defun coq-Compile coq-Compile688,25347 (defun coq-intros coq-intros695,25528 (define-key coq-keymap coq-keymap712,26205 (define-key coq-keymap coq-keymap713,26256 (define-key coq-keymap coq-keymap714,26315 (define-key coq-keymap coq-keymap715,26373 (define-key coq-keymap coq-keymap716,26429 (define-key coq-keymap coq-keymap717,26484 (define-key coq-keymap coq-keymap718,26534 (define-key coq-keymap coq-keymap719,26584 (define-key coq-keymap coq-keymap720,26634 (defun coq-guess-command-line coq-guess-command-line739,27486 (defun coq-pre-shell-start coq-pre-shell-start761,28293 (defun coq-mode-config coq-mode-config773,28817 (defun coq-shell-mode-config coq-shell-mode-config873,32330 (defun coq-goals-mode-config coq-goals-mode-config912,33981 (defun coq-response-config coq-response-config920,34229 (defun coq-maybe-compile-buffer coq-maybe-compile-buffer941,34956 (defun coq-ancestors-of coq-ancestors-of978,36490 (defun coq-all-ancestors-of coq-all-ancestors-of1001,37457 (defconst coq-require-command-regexp coq-require-command-regexp1013,37850 (defun coq-process-require-command coq-process-require-command1018,38059 (defun coq-included-children coq-included-children1023,38186 (defun coq-process-file coq-process-file1044,39025 (defpacustom print-fully-explicit print-fully-explicit1066,39823 (defpacustom print-coercions print-coercions1071,39972 (defpacustom print-match-wildcards print-match-wildcards1076,40117 (defpacustom time-commands time-commands1082,40301 (defpacustom auto-compile-vos auto-compile-vos1086,40412 (defpacustom translate-to-v8 translate-to-v81108,41367 (defun coq-preprocessing coq-preprocessing1117,41583 (defun coq-fake-constant-markup coq-fake-constant-markup1132,42002 (defun coq-create-span-menu coq-create-span-menu1154,42809 coq/coq-indent.el,1791 (defconst coq-any-command-regexpcoq-any-command-regexp11,262 (defconst coq-indent-inner-regexpcoq-indent-inner-regexp15,354 (defconst coq-indent-open-regexpcoq-indent-open-regexp43,1113 (defconst coq-indent-close-regexpcoq-indent-close-regexp48,1283 (defconst coq-indent-closepar-regexp coq-indent-closepar-regexp53,1441 (defconst coq-indent-closematch-regexp coq-indent-closematch-regexp55,1487 (defconst coq-indent-openpar-regexp coq-indent-openpar-regexp57,1559 (defconst coq-indent-openmatch-regexp coq-indent-openmatch-regexp59,1604 (defconst coq-indent-any-regexpcoq-indent-any-regexp61,1685 (defconst coq-indent-kw coq-indent-kw70,1914 (defconst coq-indent-pattern-regexp coq-indent-pattern-regexp81,2331 (defun coq-find-command-start coq-find-command-start86,2418 (defun coq-find-real-start coq-find-real-start95,2694 (defun coq-find-end coq-find-end107,3088 (defun coq-current-command-string coq-current-command-string118,3486 (defun is-at-a-space-or-tab is-at-a-space-or-tab126,3685 (defun only-spaces-on-line only-spaces-on-line132,3889 (defun find-reg find-reg139,4137 (defun coq-back-to-indentation-prevline coq-back-to-indentation-prevline154,4534 (defun coq-find-unclosed coq-find-unclosed183,5787 (defun coq-find-at-same-level-zero coq-find-at-same-level-zero210,6968 (defun coq-find-unopened coq-find-unopened238,8052 (defun coq-find-last-unopened coq-find-last-unopened284,9405 (defun coq-end-offset coq-end-offset297,9809 (defun coq-indent-command-offset coq-indent-command-offset325,10628 (defun coq-indent-expr-offset coq-indent-expr-offset370,12387 (defun coq-indent-offset coq-indent-offset482,16590 (defun coq-indent-calculate coq-indent-calculate502,17253 (defun proof-indent-line proof-indent-line516,17700 coq/coq-syntax.el,2992 (defvar coq-version-is-V8 coq-version-is-V819,648 (defvar coq-version-is-V8-0 coq-version-is-V8-021,727 (defvar coq-version-is-V8-1 coq-version-is-V8-128,1099 (defvar coq-keywords-declcoq-keywords-decl75,2947 (defvar coq-keywords-defncoq-keywords-defn90,3303 (defvar coq-keywords-goalcoq-keywords-goal109,3728 (defun coq-count-match coq-count-match152,5363 (defun coq-goal-command-p coq-goal-command-p164,5783 (defvar coq-keywords-save-strictcoq-keywords-save-strict182,6365 (defvar coq-keywords-savecoq-keywords-save190,6462 (defun coq-save-command-p coq-save-command-p194,6538 (defvar coq-keywords-kill-goal coq-keywords-kill-goal202,6817 (defcustom coq-user-state-changing-commands coq-user-state-changing-commands208,6867 (defcustom coq-user-state-preserving-commands coq-user-state-preserving-commands220,7264 (defvar coq-keywords-state-preserving-commandscoq-keywords-state-preserving-commands233,7704 (defvar coq-keywords-state-changing-misc-commandscoq-keywords-state-changing-misc-commands281,8831 (defvar coq-keywords-state-changing-commandscoq-keywords-state-changing-commands354,10812 (defvar coq-keywords-commandscoq-keywords-commands364,11009 (defvar coq-tacticalscoq-tacticals369,11158 (defvar coq-reservedcoq-reserved381,11359 (defcustom coq-user-state-changing-tactics coq-user-state-changing-tactics406,11618 (defvar coq-state-changing-tacticscoq-state-changing-tactics417,12044 (defcustom coq-user-state-preserving-tactics coq-user-state-preserving-tactics525,13628 (defvar coq-state-preserving-tacticscoq-state-preserving-tactics536,14042 (defvar coq-tacticscoq-tactics540,14140 (defvar coq-retractable-instructcoq-retractable-instruct543,14229 (defvar coq-non-retractable-instructcoq-non-retractable-instruct546,14339 (defvar coq-keywordscoq-keywords550,14461 (defvar coq-symbolscoq-symbols557,14628 (defvar coq-error-regexp coq-error-regexp575,14832 (defvar coq-id coq-id578,15061 (defvar coq-id-shy coq-id-shy579,15086 (defvar coq-ids coq-ids581,15140 (defun coq-first-abstr-regexp coq-first-abstr-regexp583,15177 (defun coq-next-abstr-regexp coq-next-abstr-regexp586,15265 (defvar coq-font-lock-termscoq-font-lock-terms589,15343 (defconst coq-save-command-regexp-strictcoq-save-command-regexp-strict604,15996 (defconst coq-save-command-regexpcoq-save-command-regexp606,16109 (defconst coq-save-with-hole-regexpcoq-save-with-hole-regexp608,16208 (defconst coq-goal-command-regexpcoq-goal-command-regexp611,16346 (defconst coq-goal-with-hole-regexpcoq-goal-with-hole-regexp613,16445 (defconst coq-decl-with-hole-regexpcoq-decl-with-hole-regexp619,16734 (defconst coq-defn-with-hole-regexpcoq-defn-with-hole-regexp622,16867 (defvar coq-font-lock-keywords-1coq-font-lock-keywords-1625,17007 (defvar coq-font-lock-keywords coq-font-lock-keywords646,18050 (defun coq-init-syntax-table coq-init-syntax-table648,18108 (defconst coq-generic-expressioncoq-generic-expression677,19006 coq/x-symbol-coq.el,2822 (defvar x-symbol-coq-required-fonts x-symbol-coq-required-fonts16,384 (defvar x-symbol-coq-name x-symbol-coq-name24,785 (defvar x-symbol-coq-modeline-name x-symbol-coq-modeline-name25,825 (defcustom x-symbol-coq-header-groups-alist x-symbol-coq-header-groups-alist27,868 (defcustom x-symbol-coq-electric-ignore x-symbol-coq-electric-ignore34,1086 (defvar x-symbol-coq-required-fonts x-symbol-coq-required-fonts41,1331 (defvar x-symbol-coq-extra-menu-items x-symbol-coq-extra-menu-items44,1430 (defvar x-symbol-coq-token-grammarx-symbol-coq-token-grammar48,1518 (defun x-symbol-coq-default-token-list x-symbol-coq-default-token-list64,2184 (defvar x-symbol-coq-user-table x-symbol-coq-user-table76,2472 (defvar x-symbol-coq-generated-data x-symbol-coq-generated-data79,2578 (defvar x-symbol-coq-master-directory x-symbol-coq-master-directory87,2816 (defvar x-symbol-coq-image-searchpath x-symbol-coq-image-searchpath88,2864 (defvar x-symbol-coq-image-cached-dirs x-symbol-coq-image-cached-dirs89,2911 (defvar x-symbol-coq-image-file-truename-alist x-symbol-coq-image-file-truename-alist90,2976 (defvar x-symbol-coq-image-keywords x-symbol-coq-image-keywords91,3028 (defcustom x-symbol-coq-subscript-matcher x-symbol-coq-subscript-matcher98,3256 (defcustom x-symbol-coq-font-lock-regexp x-symbol-coq-font-lock-regexp104,3488 (defcustom x-symbol-coq-font-lock-limit-regexp x-symbol-coq-font-lock-limit-regexp109,3660 (defcustom x-symbol-coq-font-lock-contents-regexp x-symbol-coq-font-lock-contents-regexp115,3848 (defcustom x-symbol-coq-single-char-regexp x-symbol-coq-single-char-regexp122,4102 (defun x-symbol-coq-subscript-matcher x-symbol-coq-subscript-matcher127,4250 (defun coq-match-subscript coq-match-subscript162,5939 (defvar x-symbol-coq-font-lock-allowed-faces x-symbol-coq-font-lock-allowed-faces169,6113 (defcustom x-symbol-coq-class-alistx-symbol-coq-class-alist174,6338 (defcustom x-symbol-coq-class-face-alist x-symbol-coq-class-face-alist185,6716 (defvar x-symbol-coq-font-lock-keywords x-symbol-coq-font-lock-keywords195,7026 (defvar x-symbol-coq-font-lock-allowed-faces x-symbol-coq-font-lock-allowed-faces197,7072 (defvar x-symbol-coq-case-insensitive x-symbol-coq-case-insensitive203,7296 (defvar x-symbol-coq-token-shape x-symbol-coq-token-shape204,7339 (defvar x-symbol-coq-input-token-ignore x-symbol-coq-input-token-ignore205,7377 (defvar x-symbol-coq-token-list x-symbol-coq-token-list206,7422 (defvar x-symbol-coq-symbol-table x-symbol-coq-symbol-table208,7466 (defvar x-symbol-coq-xsymbol-table x-symbol-coq-xsymbol-table312,9885 (defun x-symbol-coq-prepare-table x-symbol-coq-prepare-table459,13753 (defvar x-symbol-coq-tablex-symbol-coq-table468,14020 (defcustom x-symbol-coq-auto-stylex-symbol-coq-auto-style475,14181 demoisa/demoisa-easy.el,0 demoisa/demoisa.el,568 (defcustom isabelledemo-prog-name isabelledemo-prog-name54,1809 (defcustom isabelledemo-web-pageisabelledemo-web-page59,1931 (defun demoisa-config demoisa-config70,2161 (defun demoisa-shell-config demoisa-shell-config90,2910 (define-derived-mode demoisa-mode demoisa-mode119,3994 (define-derived-mode demoisa-shell-mode demoisa-shell-mode124,4117 (define-derived-mode demoisa-response-mode demoisa-response-mode129,4260 (define-derived-mode demoisa-goals-mode demoisa-goals-mode133,4387 (defun demoisa-pre-shell-start demoisa-pre-shell-start152,5169 generic/pg-assoc.el,408 (define-derived-mode proof-universal-keys-only-mode proof-universal-keys-only-mode20,563 (defun proof-associated-buffers proof-associated-buffers32,987 (defun pg-assoc-strip-subterm-markup pg-assoc-strip-subterm-markup46,1287 (defun pg-assoc-strip-subterm-markup-buf pg-assoc-strip-subterm-markup-buf72,2220 (defun pg-assoc-strip-subterm-markup-buf-old pg-assoc-strip-subterm-markup-buf-old94,2969 generic/pg-autotest.el,705 (defvar pg-autotest-success pg-autotest-success20,514 (defun pg-autotest-find-file pg-autotest-find-file24,598 (defun pg-autotest-find-file-restart pg-autotest-find-file-restart31,869 (defmacro pg-autotest pg-autotest44,1317 (defun pg-autotest-script-wholefile pg-autotest-script-wholefile58,1665 (defun pg-autotest-retract-file pg-autotest-retract-file75,2278 (defun pg-autotest-assert-processed pg-autotest-assert-processed81,2414 (defun pg-autotest-assert-unprocessed pg-autotest-assert-unprocessed88,2660 (defun pg-autotest-message pg-autotest-message95,2907 (defun pg-autotest-quit-prover pg-autotest-quit-prover102,3100 (defun pg-autotest-finished pg-autotest-finished108,3282 generic/pg-goals.el,1075 (define-derived-mode proof-goals-mode proof-goals-mode28,651 (define-key proof-goals-mode-map proof-goals-mode-map48,1341 (define-key proof-goals-mode-map proof-goals-mode-map51,1424 (define-key proof-goals-mode-map proof-goals-mode-map52,1494 (define-key proof-goals-mode-map proof-goals-mode-map60,2084 (define-key proof-goals-mode-map proof-goals-mode-map62,2157 (define-key proof-goals-mode-map proof-goals-mode-map63,2225 (define-key proof-goals-mode-map proof-goals-mode-map69,2659 (defun proof-goals-config-done proof-goals-config-done84,2923 (defun pg-goals-display pg-goals-display94,3211 (defun pg-goals-analyse-structure pg-goals-analyse-structure143,5154 (defun pg-goals-make-top-span pg-goals-make-top-span267,10000 (defun pg-goals-yank-subterm pg-goals-yank-subterm297,11007 (defun pg-goals-button-action pg-goals-button-action324,11907 (defun proof-expand-path proof-expand-path345,12880 (defun pg-goals-construct-command pg-goals-construct-command354,13124 (defun pg-goals-get-subterm-help pg-goals-get-subterm-help378,13976 generic/pg-metadata.el,204 (defcustom pg-metadata-default-directory pg-metadata-default-directory23,628 (defface proof-preparsed-span proof-preparsed-span28,802 (defun pg-metadata-filename-for pg-metadata-filename-for39,1065 generic/pg-pbrpm.el,2734 (defvar pg-pbrpm-use-buffer-menu pg-pbrpm-use-buffer-menu11,259 (defvar pg-pbrpm-buffer-menu pg-pbrpm-buffer-menu13,378 (defvar pg-pbrpm-spans pg-pbrpm-spans14,412 (defvar pg-pbrpm-goal-description pg-pbrpm-goal-description15,440 (defun pg-pbrpm-erase-buffer-menu pg-pbrpm-erase-buffer-menu17,480 (defun pg-pbrpm-menu-change-hook pg-pbrpm-menu-change-hook24,685 (defun pg-pbrpm-create-reset-buffer-menu pg-pbrpm-create-reset-buffer-menu42,1262 (defun pg-pbrpm-analyse-goal-buffer pg-pbrpm-analyse-goal-buffer57,1914 (defun pg-pbrpm-button-action pg-pbrpm-button-action118,4334 (defun pg-pbrpm-exists pg-pbrpm-exists125,4560 (defun pg-pbrpm-eliminate-id pg-pbrpm-eliminate-id129,4672 (defun pg-pbrpm-build-menu pg-pbrpm-build-menu137,4920 (defun pg-pbrpm-setup-span pg-pbrpm-setup-span193,7110 (defun pg-pbrpm-run-command pg-pbrpm-run-command253,9477 (defun pg-pbrpm-get-pos-info pg-pbrpm-get-pos-info281,10753 (defun pg-pbrpm-get-region-info pg-pbrpm-get-region-info317,11895 (defun auto-select-arround-pos auto-select-arround-pos327,12220 (defun pg-pbrpm-translate-position pg-pbrpm-translate-position339,12664 (defun pg-pbrpm-process-click pg-pbrpm-process-click345,12888 (defvar pg-pbrpm-remember-region-selected-region pg-pbrpm-remember-region-selected-region365,13892 (defvar pg-pbrpm-regions-list pg-pbrpm-regions-list366,13946 (defun pg-pbrpm-erase-regions-list pg-pbrpm-erase-regions-list368,13982 (defun pg-pbrpm-filter-regions-list pg-pbrpm-filter-regions-list377,14291 (defface pg-pbrpm-multiple-selection-facepg-pbrpm-multiple-selection-face384,14554 (defface pg-pbrpm-menu-input-facepg-pbrpm-menu-input-face392,14759 (defun pg-pbrpm-do-remember-region pg-pbrpm-do-remember-region400,14952 (defun pg-pbrpm-remember-region-drag-up-hook pg-pbrpm-remember-region-drag-up-hook421,15793 (defun pg-pbrpm-remember-region-click-hook pg-pbrpm-remember-region-click-hook425,15964 (defun pg-pbrpm-remember-region pg-pbrpm-remember-region430,16149 (defun pg-pbrpm-process-region pg-pbrpm-process-region444,16864 (defun pg-pbrpm-process-regions-list pg-pbrpm-process-regions-list461,17587 (defun pg-pbrpm-region-expression pg-pbrpm-region-expression465,17770 (define-key proof-goals-mode-map proof-goals-mode-map489,18706 (define-key proof-goals-mode-map proof-goals-mode-map490,18776 (define-key proof-goals-mode-map proof-goals-mode-map491,18853 (define-key pg-span-context-menu-keymap pg-span-context-menu-keymap492,18933 (define-key pg-span-context-menu-keymap pg-span-context-menu-keymap493,19010 (define-key proof-mode-map proof-mode-map494,19093 (define-key proof-mode-map proof-mode-map495,19157 (define-key proof-mode-map proof-mode-map496,19228 generic/pg-pgip.el,5296 (defalias 'pg-pgip-debug pg-pgip-debug29,894 (defalias 'pg-pgip-error pg-pgip-error30,935 (defalias 'pg-pgip-warning pg-pgip-warning31,970 (defconst pg-pgip-version-supported pg-pgip-version-supported33,1020 (defun pg-pgip-process-packet pg-pgip-process-packet37,1126 (defvar pg-pgip-last-seen-id pg-pgip-last-seen-id47,1699 (defvar pg-pgip-last-seen-seq pg-pgip-last-seen-seq48,1733 (defun pg-pgip-process-pgip pg-pgip-process-pgip50,1769 (defun pg-pgip-process-msg pg-pgip-process-msg69,2696 (defvar pg-pgip-post-process-functionspg-pgip-post-process-functions83,3266 (defun pg-pgip-post-process pg-pgip-post-process93,3750 (defun pg-pgip-process-askpgip pg-pgip-process-askpgip109,4361 (defun pg-pgip-process-usespgip pg-pgip-process-usespgip114,4520 (defun pg-pgip-process-usespgml pg-pgip-process-usespgml118,4684 (defun pg-pgip-process-pgmlconfig pg-pgip-process-pgmlconfig122,4848 (defun pg-pgip-process-proverinfo pg-pgip-process-proverinfo138,5456 (defun pg-pgip-process-hasprefs pg-pgip-process-hasprefs155,6121 (defun pg-pgip-haspref pg-pgip-haspref169,6753 (defun pg-pgip-process-prefval pg-pgip-process-prefval188,7532 (defun pg-pgip-process-guiconfig pg-pgip-process-guiconfig215,8241 (defvar proof-assistant-idtables proof-assistant-idtables222,8358 (defun pg-pgip-process-ids pg-pgip-process-ids225,8475 (defun pg-complete-idtable-symbol pg-complete-idtable-symbol251,9554 (defalias 'pg-pgip-process-setids pg-pgip-process-setids256,9646 (defalias 'pg-pgip-process-addids pg-pgip-process-addids257,9702 (defalias 'pg-pgip-process-delids pg-pgip-process-delids258,9758 (defun pg-pgip-process-idvalue pg-pgip-process-idvalue261,9816 (defun pg-pgip-process-menuadd pg-pgip-process-menuadd273,10153 (defun pg-pgip-process-menudel pg-pgip-process-menudel276,10196 (defun pg-pgip-process-ready pg-pgip-process-ready285,10429 (defun pg-pgip-process-cleardisplay pg-pgip-process-cleardisplay288,10470 (defun pg-pgip-process-proofstate pg-pgip-process-proofstate302,10947 (defun pg-pgip-process-normalresponse pg-pgip-process-normalresponse306,11024 (defun pg-pgip-process-errorresponse pg-pgip-process-errorresponse310,11148 (defun pg-pgip-process-scriptinsert pg-pgip-process-scriptinsert314,11271 (defun pg-pgip-process-metainforesponse pg-pgip-process-metainforesponse319,11405 (defun pg-pgip-process-informfileloaded pg-pgip-process-informfileloaded328,11646 (defun pg-pgip-process-informfileretracted pg-pgip-process-informfileretracted334,11912 (defun pg-pgip-process-brokerstatus pg-pgip-process-brokerstatus347,12386 (defun pg-pgip-process-proveravailmsg pg-pgip-process-proveravailmsg350,12434 (defun pg-pgip-process-newprovermsg pg-pgip-process-newprovermsg353,12484 (defun pg-pgip-process-proverstatusmsg pg-pgip-process-proverstatusmsg356,12532 (defvar pg-pgip-srcids pg-pgip-srcids365,12779 (defun pg-pgip-process-newfile pg-pgip-process-newfile369,12886 (defun pg-pgip-process-filestatus pg-pgip-process-filestatus385,13474 (defun pg-pgip-process-newobj pg-pgip-process-newobj405,14129 (defun pg-pgip-process-delobj pg-pgip-process-delobj408,14171 (defun pg-pgip-process-objectstatus pg-pgip-process-objectstatus411,14213 (defun pg-pgip-process-parsescript pg-pgip-process-parsescript425,14569 (defun pg-pgip-get-pgiptype pg-pgip-get-pgiptype448,15444 (defun pg-pgip-default-for pg-pgip-default-for468,16239 (defun pg-pgip-subst-for pg-pgip-subst-for481,16634 (defun pg-pgip-interpret-value pg-pgip-interpret-value493,16977 (defun pg-pgip-interpret-choice pg-pgip-interpret-choice511,17660 (defun pg-pgip-get-icon pg-pgip-get-icon542,18733 (defsubst pg-pgip-get-name pg-pgip-get-name546,18881 (defsubst pg-pgip-get-version pg-pgip-get-version549,18998 (defsubst pg-pgip-get-descr pg-pgip-get-descr552,19121 (defsubst pg-pgip-get-thmname pg-pgip-get-thmname555,19240 (defsubst pg-pgip-get-thyname pg-pgip-get-thyname558,19363 (defsubst pg-pgip-get-url pg-pgip-get-url561,19486 (defsubst pg-pgip-get-srcid pg-pgip-get-srcid564,19601 (defsubst pg-pgip-get-proverid pg-pgip-get-proverid567,19720 (defsubst pg-pgip-get-symname pg-pgip-get-symname570,19845 (defsubst pg-pgip-get-prefcat pg-pgip-get-prefcat573,19965 (defsubst pg-pgip-get-default pg-pgip-get-default576,20093 (defsubst pg-pgip-get-objtype pg-pgip-get-objtype579,20216 (defsubst pg-pgip-get-value pg-pgip-get-value582,20339 (defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext585,20409 (defun pg-pgip-get-pgmltext pg-pgip-get-pgmltext587,20468 (defun pg-pgip-string-of-command pg-pgip-string-of-command596,20703 (defconst pg-pgip-idpg-pgip-id613,21464 (defvar pg-pgip-refseq pg-pgip-refseq619,21744 (defvar pg-pgip-refid pg-pgip-refid621,21842 (defvar pg-pgip-seq pg-pgip-seq624,21936 (defun pg-pgip-assemble-packet pg-pgip-assemble-packet626,22000 (defun pg-pgip-issue pg-pgip-issue644,22815 (defun pg-pgip-maybe-askpgip pg-pgip-maybe-askpgip661,23428 (defun pg-pgip-askprefs pg-pgip-askprefs667,23619 (defun pg-pgip-askids pg-pgip-askids671,23733 (defun pg-pgip-reset pg-pgip-reset684,24024 (defconst pg-pgip-start-element-regexp pg-pgip-start-element-regexp715,24722 (defconst pg-pgip-end-element-regexp pg-pgip-end-element-regexp716,24774 generic/pg-pgip-old.el,734 (defun pg-pgip-process-oldhaspref pg-pgip-process-oldhaspref18,633 (defun pg-pgip-process-haspref pg-pgip-process-haspref21,730 (defun pg-pgip-old-interpret-bool pg-pgip-old-interpret-bool57,2158 (defun pg-pgip-old-interpret-int pg-pgip-old-interpret-int66,2442 (defun pg-pgip-old-interpret-string pg-pgip-old-interpret-string71,2609 (defun pg-pgip-old-interpret-choice pg-pgip-old-interpret-choice74,2663 (defun pg-pgip-old-interpret-value pg-pgip-old-interpret-value94,3382 (defun pg-pgip-old-default-for pg-pgip-old-default-for113,3928 (defun pg-pgip-old-subst-for pg-pgip-old-subst-for124,4252 (defun pg-pgip-old-get-type pg-pgip-old-get-type131,4417 (defun pg-pgip-old-pgiptype pg-pgip-old-pgiptype138,4633 generic/pg-response.el,1890 (define-derived-mode proof-response-mode proof-response-mode24,597 (defun proof-response-config-done proof-response-config-done47,1490 (defvar proof-shell-special-display-regexp proof-shell-special-display-regexp68,2265 (defconst proof-multiframe-specifiers proof-multiframe-specifiers76,2670 (defun proof-map-multiple-frame-specifiers proof-map-multiple-frame-specifiers85,3034 (defconst proof-multiframe-parametersproof-multiframe-parameters95,3496 (defun proof-multiple-frames-enable proof-multiple-frames-enable104,3795 (defun proof-three-window-enable proof-three-window-enable126,4515 (defun proof-select-three-b proof-select-three-b130,4579 (defun proof-display-three-b proof-display-three-b145,5048 (defvar pg-frame-configuration pg-frame-configuration159,5542 (defun pg-cache-frame-configuration pg-cache-frame-configuration163,5689 (defun proof-layout-windows proof-layout-windows167,5860 (defun proof-delete-other-frames proof-delete-other-frames208,7673 (defvar pg-response-erase-flag pg-response-erase-flag239,8768 (defun proof-shell-maybe-erase-responseproof-shell-maybe-erase-response242,8883 (defun pg-response-display pg-response-display272,10033 (defun pg-response-display-with-face pg-response-display-with-face289,10855 (defun pg-response-clear-displays pg-response-clear-displays324,12212 (defvar pg-response-next-error pg-response-next-error341,12742 (defun proof-next-error proof-next-error345,12864 (defun pg-response-has-error-location pg-response-has-error-location425,15798 (defvar proof-trace-last-fontify-pos proof-trace-last-fontify-pos448,16631 (defun proof-trace-fontify-pos proof-trace-fontify-pos450,16674 (defun proof-trace-buffer-display proof-trace-buffer-display458,16988 (defun proof-trace-buffer-finish proof-trace-buffer-finish482,17961 (defun pg-thms-buffer-clear pg-thms-buffer-clear503,18486 generic/pg-thymodes.el,219 (defmacro pg-defthymode pg-defthymode19,466 (defmacro pg-do-unless-null pg-do-unless-null67,2277 (defun pg-symval pg-symval72,2364 (defun pg-modesym pg-modesym78,2520 (defun pg-modesymval pg-modesymval82,2634 generic/pg-user.el,3655 (defmacro proof-maybe-save-point proof-maybe-save-point21,410 (defun proof-maybe-follow-locked-end proof-maybe-follow-locked-end29,612 (defun proof-assert-next-command-interactive proof-assert-next-command-interactive43,977 (defun proof-process-buffer proof-process-buffer53,1348 (defun proof-undo-last-successful-command proof-undo-last-successful-command67,1665 (defun proof-undo-and-delete-last-successful-command proof-undo-and-delete-last-successful-command72,1827 (defun proof-undo-last-successful-command-1 proof-undo-last-successful-command-194,2799 (defun proof-retract-buffer proof-retract-buffer110,3364 (defun proof-retract-current-goal proof-retract-current-goal119,3644 (defun proof-interrupt-process proof-interrupt-process137,4135 (defun proof-goto-command-start proof-goto-command-start164,5120 (defun proof-goto-command-end proof-goto-command-end187,6062 (defun proof-mouse-goto-point proof-mouse-goto-point212,6842 (defun proof-mouse-track-insert proof-mouse-track-insert227,7416 (defvar proof-minibuffer-history proof-minibuffer-history262,8526 (defun proof-minibuffer-cmd proof-minibuffer-cmd265,8620 (defun proof-frob-locked-end proof-frob-locked-end313,10426 (defmacro proof-if-setting-configured proof-if-setting-configured406,13340 (defmacro proof-define-assistant-command proof-define-assistant-command414,13610 (defmacro proof-define-assistant-command-witharg proof-define-assistant-command-witharg427,14076 (defun proof-issue-new-command proof-issue-new-command447,14901 (defun proof-cd-sync proof-cd-sync492,16400 (deflocal proof-electric-terminator proof-electric-terminator543,17869 (defun proof-electric-terminator-enable proof-electric-terminator-enable553,18216 (defun proof-electric-term-incomment-fn proof-electric-term-incomment-fn564,18703 (defun proof-process-electric-terminator proof-process-electric-terminator584,19459 (defun proof-electric-terminator proof-electric-terminator611,20610 (defun proof-add-completions proof-add-completions633,21248 (defun proof-script-complete proof-script-complete653,22005 (defun pg-insert-last-output-as-comment pg-insert-last-output-as-comment681,22596 (defun pg-copy-span-contents pg-copy-span-contents712,23824 (defun pg-numth-span-higher-or-lower pg-numth-span-higher-or-lower729,24384 (defun pg-control-span-of pg-control-span-of755,25135 (defun pg-move-span-contents pg-move-span-contents761,25339 (defun pg-fixup-children-span pg-fixup-children-span815,27563 (defun pg-move-region-down pg-move-region-down822,27771 (defun pg-move-region-up pg-move-region-up831,28065 (defun proof-forward-command proof-forward-command861,28905 (defun proof-backward-command proof-backward-command882,29627 (defvar pg-span-context-menu-keymappg-span-context-menu-keymap898,29871 (defun pg-span-for-event pg-span-for-event914,30298 (defun pg-span-context-menu pg-span-context-menu925,30682 (defun pg-toggle-visibility pg-toggle-visibility940,31142 (defun pg-create-in-span-context-menu pg-create-in-span-context-menu950,31464 (defun pg-goals-buffers-hint pg-goals-buffers-hint1022,34017 (defun pg-slow-fontify-tracing-hint pg-slow-fontify-tracing-hint1025,34184 (defun pg-response-buffers-hint pg-response-buffers-hint1028,34340 (defun pg-jump-to-end-hint pg-jump-to-end-hint1037,34689 (defun pg-processing-complete-hint pg-processing-complete-hint1040,34805 (defun pg-next-error-hint pg-next-error-hint1056,35491 (defun pg-hint pg-hint1060,35628 (defun pg-identifier-under-mouse-query pg-identifier-under-mouse-query1079,36304 (defun proof-imenu-enable proof-imenu-enable1124,37931 generic/pg-xhtml.el,573 (defvar pg-xhtml-dir pg-xhtml-dir17,423 (defun pg-xhtml-dir pg-xhtml-dir20,489 (defvar pg-xhtml-file-count pg-xhtml-file-count32,856 (defun pg-xhtml-next-file pg-xhtml-next-file35,928 (defvar pg-xhtml-header pg-xhtml-header47,1159 (defmacro pg-xhtml-write-tempfile pg-xhtml-write-tempfile53,1400 (defun pg-xhtml-cleanup-tempdir pg-xhtml-cleanup-tempdir71,1990 (defvar pg-mozilla-prog-name pg-mozilla-prog-name75,2121 (defun pg-xhtml-display-file-mozilla pg-xhtml-display-file-mozilla79,2229 (defalias 'pg-xhtml-display-file pg-xhtml-display-file84,2402 generic/pg-xml.el,670 (defun pg-xml-parse-string pg-xml-parse-string38,1118 (defun pg-xml-parse-buffer pg-xml-parse-buffer49,1452 (defun pg-xml-get-attr pg-xml-get-attr71,2185 (defun pg-xml-child-elts pg-xml-child-elts79,2489 (defun pg-xml-child-elt pg-xml-child-elt84,2694 (defun pg-xml-get-child pg-xml-get-child92,2977 (defun pg-xml-get-text-content pg-xml-get-text-content102,3349 (defmacro pg-xml-attr pg-xml-attr113,3699 (defmacro pg-xml-node pg-xml-node115,3761 (defconst pg-xml-header pg-xml-header118,3854 (defun pg-xml-string-of pg-xml-string-of122,3931 (defun pg-xml-output-internal pg-xml-output-internal133,4303 (defun pg-xml-cdata pg-xml-cdata167,5453 generic/_pkg.el,0 generic/proof-autoloads.el,79 (defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region246,9930 generic/proof-config.el,16776 (defgroup proof-user-options proof-user-options84,3173 (defcustom proof-electric-terminator-enable proof-electric-terminator-enable89,3287 (defcustom proof-toolbar-enable proof-toolbar-enable101,3821 (defcustom proof-imenu-enable proof-imenu-enable107,3994 (defpgcustom x-symbol-enable x-symbol-enable113,4165 (defpgcustom mmm-enable mmm-enable122,4515 (defcustom pg-show-hints pg-show-hints131,4869 (defcustom proof-output-fontify-enable proof-output-fontify-enable136,5004 (defcustom proof-trace-output-slow-catchup proof-trace-output-slow-catchup146,5386 (defcustom proof-strict-state-preserving proof-strict-state-preserving156,5884 (defcustom proof-strict-read-only proof-strict-read-only169,6493 (defcustom proof-three-window-enable proof-three-window-enable179,6843 (defcustom proof-multiple-frames-enable proof-multiple-frames-enable198,7598 (defcustom proof-delete-empty-windows proof-delete-empty-windows207,7934 (defcustom proof-shrink-windows-tofit proof-shrink-windows-tofit218,8465 (defcustom proof-toolbar-use-button-enablers proof-toolbar-use-button-enablers225,8737 (defcustom proof-query-file-save-when-activating-scripting proof-query-file-save-when-activating-scripting248,9609 (defpgcustom script-indent script-indent264,10332 (defcustom proof-one-command-per-line proof-one-command-per-line270,10520 (defcustom proof-prog-name-ask proof-prog-name-ask278,10740 (defcustom proof-prog-name-guess proof-prog-name-guess284,10901 (defcustom proof-tidy-responseproof-tidy-response292,11161 (defcustom proof-show-debug-messages proof-show-debug-messages306,11628 (defcustom proof-experimental-features proof-experimental-features315,12006 (defcustom proof-follow-mode proof-follow-mode333,12768 (defcustom proof-auto-action-when-deactivating-scripting proof-auto-action-when-deactivating-scripting359,13963 (defcustom proof-script-command-separator proof-script-command-separator382,14914 (defcustom proof-rsh-command proof-rsh-command390,15207 (defcustom proof-disappearing-proofs proof-disappearing-proofs406,15744 (defgroup proof-faces proof-faces433,16394 (defmacro proof-face-specs proof-face-specs438,16500 (defface proof-queue-face proof-queue-face453,16946 (defface proof-locked-faceproof-locked-face461,17226 (defface proof-declaration-name-faceproof-declaration-name-face474,17729 (defconst proof-declaration-name-face proof-declaration-name-face486,18122 (defface proof-tacticals-name-faceproof-tacticals-name-face491,18358 (defconst proof-tacticals-name-face proof-tacticals-name-face500,18620 (defface proof-tactics-name-faceproof-tactics-name-face505,18850 (defconst proof-tactics-name-face proof-tactics-name-face514,19115 (defface proof-error-face proof-error-face519,19339 (defface proof-warning-faceproof-warning-face527,19546 (defface proof-eager-annotation-faceproof-eager-annotation-face536,19803 (defface proof-debug-message-faceproof-debug-message-face544,20021 (defface proof-boring-faceproof-boring-face552,20220 (defface proof-mouse-highlight-faceproof-mouse-highlight-face560,20412 (defface proof-highlight-dependent-faceproof-highlight-dependent-face568,20608 (defface proof-highlight-dependency-faceproof-highlight-dependency-face576,20817 (defgroup prover-config prover-config594,21076 (defcustom proof-mode-for-shell proof-mode-for-shell628,22195 (defcustom proof-mode-for-response proof-mode-for-response635,22442 (defcustom proof-mode-for-goals proof-mode-for-goals642,22725 (defcustom proof-mode-for-script proof-mode-for-script649,22980 (defcustom proof-guess-command-line proof-guess-command-line660,23414 (defcustom proof-assistant-home-page proof-assistant-home-page675,23911 (defcustom proof-context-command proof-context-command681,24081 (defcustom proof-info-command proof-info-command686,24215 (defcustom proof-showproof-command proof-showproof-command693,24487 (defcustom proof-goal-command proof-goal-command698,24623 (defcustom proof-save-command proof-save-command706,24921 (defcustom proof-find-theorems-command proof-find-theorems-command714,25231 (defconst proof-toolbar-entries-defaultproof-toolbar-entries-default721,25540 (defpgcustom toolbar-entries toolbar-entries752,27272 (defcustom proof-assistant-true-value proof-assistant-true-value770,27993 (defcustom proof-assistant-false-value proof-assistant-false-value776,28183 (defcustom proof-assistant-format-int-fn proof-assistant-format-int-fn782,28377 (defcustom proof-assistant-format-string-fn proof-assistant-format-string-fn789,28626 (defcustom proof-assistant-setting-format proof-assistant-setting-format796,28893 (defgroup proof-script proof-script818,29588 (defcustom proof-terminal-char proof-terminal-char823,29718 (defcustom proof-script-sexp-commands proof-script-sexp-commands833,30122 (defcustom proof-script-command-end-regexp proof-script-command-end-regexp844,30592 (defcustom proof-script-command-start-regexp proof-script-command-start-regexp862,31411 (defcustom proof-script-use-old-parser proof-script-use-old-parser873,31873 (defcustom proof-script-integral-proofs proof-script-integral-proofs885,32362 (defcustom proof-script-fly-past-comments proof-script-fly-past-comments900,33018 (defcustom proof-script-parse-function proof-script-parse-function907,33335 (defcustom proof-script-comment-start proof-script-comment-start925,33981 (defcustom proof-script-comment-start-regexp proof-script-comment-start-regexp936,34416 (defcustom proof-script-comment-end proof-script-comment-end944,34733 (defcustom proof-script-comment-end-regexp proof-script-comment-end-regexp956,35151 (defcustom pg-insert-output-as-comment-fn pg-insert-output-as-comment-fn964,35462 (defcustom proof-string-start-regexp proof-string-start-regexp970,35714 (defcustom proof-string-end-regexp proof-string-end-regexp975,35879 (defcustom proof-case-fold-search proof-case-fold-search980,36040 (defcustom proof-save-command-regexp proof-save-command-regexp989,36456 (defcustom proof-save-with-hole-regexp proof-save-with-hole-regexp994,36567 (defcustom proof-save-with-hole-result proof-save-with-hole-result1006,37019 (defcustom proof-goal-command-regexp proof-goal-command-regexp1017,37483 (defcustom proof-goal-with-hole-regexp proof-goal-with-hole-regexp1026,37875 (defcustom proof-goal-with-hole-result proof-goal-with-hole-result1038,38319 (defcustom proof-non-undoables-regexp proof-non-undoables-regexp1048,38718 (defcustom proof-nested-undo-regexp proof-nested-undo-regexp1059,39174 (defcustom proof-ignore-for-undo-count proof-ignore-for-undo-count1075,39886 (defcustom proof-script-next-entity-regexps proof-script-next-entity-regexps1083,40189 (defcustom proof-script-find-next-entity-fnproof-script-find-next-entity-fn1127,41923 (defcustom proof-script-imenu-generic-expression proof-script-imenu-generic-expression1147,42753 (defcustom proof-goal-command-p proof-goal-command-p1162,43414 (defcustom proof-really-save-command-p proof-really-save-command-p1189,44850 (defcustom proof-completed-proof-behaviour proof-completed-proof-behaviour1201,45311 (defcustom proof-count-undos-fn proof-count-undos-fn1229,46671 (defconst proof-no-command proof-no-command1264,48272 (defcustom proof-find-and-forget-fn proof-find-and-forget-fn1269,48476 (defcustom proof-forget-id-command proof-forget-id-command1286,49187 (defcustom pg-topterm-goalhyp-fn pg-topterm-goalhyp-fn1296,49545 (defcustom proof-kill-goal-command proof-kill-goal-command1308,50026 (defcustom proof-undo-n-times-cmd proof-undo-n-times-cmd1322,50536 (defcustom proof-nested-goals-history-p proof-nested-goals-history-p1336,51085 (defcustom proof-state-preserving-p proof-state-preserving-p1345,51423 (defcustom proof-activate-scripting-hook proof-activate-scripting-hook1355,51893 (defcustom proof-deactivate-scripting-hook proof-deactivate-scripting-hook1374,52671 (defcustom proof-indent proof-indent1387,53036 (defcustom proof-indent-pad-eol proof-indent-pad-eol1393,53210 (defcustom proof-indent-hang proof-indent-hang1400,53450 (defcustom proof-indent-enclose-offset proof-indent-enclose-offset1405,53576 (defcustom proof-indent-open-offset proof-indent-open-offset1410,53718 (defcustom proof-indent-close-offset proof-indent-close-offset1415,53855 (defcustom proof-indent-any-regexp proof-indent-any-regexp1420,53993 (defcustom proof-indent-inner-regexp proof-indent-inner-regexp1425,54153 (defcustom proof-indent-enclose-regexp proof-indent-enclose-regexp1430,54307 (defcustom proof-indent-open-regexp proof-indent-open-regexp1435,54461 (defcustom proof-indent-close-regexp proof-indent-close-regexp1440,54613 (defcustom proof-script-font-lock-keywords proof-script-font-lock-keywords1446,54767 (defcustom proof-script-syntax-table-entries proof-script-syntax-table-entries1454,55090 (defcustom proof-script-span-context-menu-extensions proof-script-span-context-menu-extensions1472,55487 (defgroup proof-shell proof-shell1498,56276 (defcustom proof-prog-name proof-prog-name1508,56447 (defcustom proof-shell-auto-terminate-commands proof-shell-auto-terminate-commands1517,56802 (defcustom proof-shell-pre-sync-init-cmd proof-shell-pre-sync-init-cmd1526,57199 (defcustom proof-shell-init-cmd proof-shell-init-cmd1540,57758 (defcustom proof-shell-restart-cmd proof-shell-restart-cmd1551,58228 (defcustom proof-shell-quit-cmd proof-shell-quit-cmd1556,58383 (defcustom proof-shell-quit-timeout proof-shell-quit-timeout1561,58550 (defcustom proof-shell-cd-cmd proof-shell-cd-cmd1571,58998 (defcustom proof-shell-start-silent-cmd proof-shell-start-silent-cmd1588,59665 (defcustom proof-shell-stop-silent-cmd proof-shell-stop-silent-cmd1597,60041 (defcustom proof-shell-silent-threshold proof-shell-silent-threshold1606,60378 (defcustom proof-shell-inform-file-processed-cmd proof-shell-inform-file-processed-cmd1614,60712 (defcustom proof-shell-inform-file-retracted-cmd proof-shell-inform-file-retracted-cmd1635,61635 (defcustom proof-auto-multiple-files proof-auto-multiple-files1663,62906 (defcustom proof-cannot-reopen-processed-files proof-cannot-reopen-processed-files1678,63627 (defcustom proof-shell-require-command-regexp proof-shell-require-command-regexp1692,64294 (defcustom proof-done-advancing-require-function proof-done-advancing-require-function1703,64756 (defcustom proof-shell-quiet-errors proof-shell-quiet-errors1709,64996 (defcustom proof-shell-prompt-pattern proof-shell-prompt-pattern1726,65334 (defcustom proof-shell-wakeup-char proof-shell-wakeup-char1736,65756 (defcustom proof-shell-annotated-prompt-regexp proof-shell-annotated-prompt-regexp1742,65987 (defcustom proof-shell-abort-goal-regexp proof-shell-abort-goal-regexp1758,66627 (defcustom proof-shell-error-regexp proof-shell-error-regexp1763,66762 (defcustom proof-shell-truncate-before-error proof-shell-truncate-before-error1783,67556 (defcustom pg-next-error-regexp pg-next-error-regexp1797,68099 (defcustom pg-next-error-filename-regexp pg-next-error-filename-regexp1812,68709 (defcustom pg-next-error-extract-filename pg-next-error-extract-filename1836,69747 (defcustom proof-shell-interrupt-regexp proof-shell-interrupt-regexp1843,69990 (defcustom proof-shell-proof-completed-regexp proof-shell-proof-completed-regexp1857,70582 (defcustom proof-shell-clear-response-regexp proof-shell-clear-response-regexp1870,71090 (defcustom proof-shell-clear-goals-regexp proof-shell-clear-goals-regexp1877,71389 (defcustom proof-shell-start-goals-regexp proof-shell-start-goals-regexp1884,71682 (defcustom proof-shell-end-goals-regexp proof-shell-end-goals-regexp1892,72049 (defcustom proof-shell-eager-annotation-start proof-shell-eager-annotation-start1898,72291 (defcustom proof-shell-eager-annotation-start-length proof-shell-eager-annotation-start-length1916,73029 (defcustom proof-shell-eager-annotation-end proof-shell-eager-annotation-end1927,73456 (defcustom proof-shell-assumption-regexp proof-shell-assumption-regexp1943,74132 (defcustom proof-shell-process-file proof-shell-process-file1953,74544 (defcustom proof-shell-retract-files-regexp proof-shell-retract-files-regexp1975,75496 (defcustom proof-shell-compute-new-files-list proof-shell-compute-new-files-list1984,75832 (defcustom pg-use-specials-for-fontify pg-use-specials-for-fontify1996,76377 (defcustom proof-shell-set-elisp-variable-regexp proof-shell-set-elisp-variable-regexp2004,76701 (defcustom proof-shell-match-pgip-cmd proof-shell-match-pgip-cmd2037,78173 (defcustom proof-shell-issue-pgip-cmd proof-shell-issue-pgip-cmd2046,78503 (defcustom proof-shell-query-dependencies-cmd proof-shell-query-dependencies-cmd2055,78859 (defcustom proof-shell-theorem-dependency-list-regexp proof-shell-theorem-dependency-list-regexp2062,79119 (defcustom proof-shell-theorem-dependency-list-split proof-shell-theorem-dependency-list-split2078,79779 (defcustom proof-shell-show-dependency-cmd proof-shell-show-dependency-cmd2087,80204 (defcustom proof-shell-identifier-under-mouse-cmd proof-shell-identifier-under-mouse-cmd2094,80473 (defcustom proof-shell-trace-output-regexp proof-shell-trace-output-regexp2117,81554 (defcustom proof-shell-thms-output-regexp proof-shell-thms-output-regexp2133,82098 (defcustom proof-shell-filename-escapes proof-shell-filename-escapes2145,82483 (defcustom proof-shell-process-connection-type proof-shell-process-connection-type2162,83163 (defcustom proof-shell-strip-crs-from-input proof-shell-strip-crs-from-input2185,84210 (defcustom proof-shell-strip-crs-from-output proof-shell-strip-crs-from-output2197,84699 (defcustom proof-shell-insert-hook proof-shell-insert-hook2205,85067 (defcustom proof-pre-shell-start-hook proof-pre-shell-start-hook2245,87031 (defcustom proof-shell-handle-delayed-output-hookproof-shell-handle-delayed-output-hook2261,87503 (defcustom proof-shell-handle-error-or-interrupt-hookproof-shell-handle-error-or-interrupt-hook2267,87718 (defcustom proof-shell-pre-interrupt-hookproof-shell-pre-interrupt-hook2282,88332 (defcustom proof-shell-process-output-system-specific proof-shell-process-output-system-specific2292,88702 (defcustom proof-state-change-hook proof-state-change-hook2311,89567 (defcustom proof-shell-font-lock-keywords proof-shell-font-lock-keywords2322,89949 (defcustom proof-shell-syntax-table-entries proof-shell-syntax-table-entries2330,90277 (defgroup proof-goals proof-goals2348,90649 (defcustom pg-subterm-first-special-char pg-subterm-first-special-char2353,90770 (defcustom pg-subterm-anns-use-stack pg-subterm-anns-use-stack2361,91082 (defcustom pg-goals-change-goal pg-goals-change-goal2370,91386 (defcustom pbp-goal-command pbp-goal-command2375,91501 (defcustom pbp-hyp-command pbp-hyp-command2380,91657 (defcustom pg-subterm-help-cmd pg-subterm-help-cmd2385,91819 (defcustom pg-goals-error-regexp pg-goals-error-regexp2392,92055 (defcustom proof-shell-result-start proof-shell-result-start2397,92215 (defcustom proof-shell-result-end proof-shell-result-end2403,92449 (defcustom pg-subterm-start-char pg-subterm-start-char2409,92662 (defcustom pg-subterm-sep-char pg-subterm-sep-char2423,93244 (defcustom pg-subterm-end-char pg-subterm-end-char2429,93423 (defcustom pg-topterm-char pg-topterm-char2435,93580 (defcustom proof-goals-font-lock-keywords proof-goals-font-lock-keywords2452,94186 (defcustom proof-resp-font-lock-keywords proof-resp-font-lock-keywords2466,94865 (defcustom pg-before-fontify-output-hook pg-before-fontify-output-hook2478,95443 (defcustom pg-after-fontify-output-hook pg-after-fontify-output-hook2486,95803 (defgroup proof-x-symbol proof-x-symbol2498,96057 (defcustom proof-xsym-extra-modes proof-xsym-extra-modes2503,96185 (defcustom proof-xsym-font-lock-keywords proof-xsym-font-lock-keywords2516,96814 (defcustom proof-xsym-activate-command proof-xsym-activate-command2524,97191 (defcustom proof-xsym-deactivate-command proof-xsym-deactivate-command2531,97427 (defpgcustom x-symbol-language x-symbol-language2538,97669 (defpgcustom favourites favourites2553,98116 (defpgcustom menu-entries menu-entries2558,98306 (defpgcustom help-menu-entries help-menu-entries2565,98543 (defpgcustom keymap keymap2572,98806 (defpgcustom completion-table completion-table2577,98977 (defpgcustom tags-program tags-program2587,99342 (defcustom proof-general-name proof-general-name2599,99515 (defcustom proof-general-home-pageproof-general-home-page2604,99672 (defcustom proof-unnamed-theorem-nameproof-unnamed-theorem-name2610,99831 (defcustom proof-universal-keysproof-universal-keys2618,100107 generic/proof-depends.el,1325 (defvar proof-thm-names-of-files proof-thm-names-of-files19,540 (defvar proof-def-names-of-files proof-def-names-of-files25,824 (defun proof-depends-module-name-for-buffer proof-depends-module-name-for-buffer34,1128 (defun proof-depends-module-of proof-depends-module-of44,1570 (defun proof-depends-names-in-same-file proof-depends-names-in-same-file52,1864 (defun proof-depends-process-dependencies proof-depends-process-dependencies71,2484 (defun proof-dependency-in-span-context-menu proof-dependency-in-span-context-menu124,4226 (defun proof-dep-alldeps-menu proof-dep-alldeps-menu147,5129 (defun proof-dep-make-alldeps-menu proof-dep-make-alldeps-menu153,5356 (defun proof-dep-split-deps proof-dep-split-deps171,5852 (defun proof-dep-make-submenu proof-dep-make-submenu192,6551 (defun proof-make-highlight-depts-menu proof-make-highlight-depts-menu202,6904 (defun proof-goto-dependency proof-goto-dependency212,7208 (defun proof-show-dependency proof-show-dependency218,7431 (defconst pg-dep-span-priority pg-dep-span-priority225,7721 (defconst pg-ordinary-span-priority pg-ordinary-span-priority226,7757 (defun proof-highlight-depcs proof-highlight-depcs228,7799 (defun proof-highlight-depts proof-highlight-depts238,8229 (defun proof-dep-unhighlight proof-dep-unhighlight249,8703 generic/proof-easy-config.el,317 (defconst proof-easy-config-derived-modes-tableproof-easy-config-derived-modes-table15,492 (defun proof-easy-config-define-derived-modes proof-easy-config-define-derived-modes22,898 (defun proof-easy-config-check-setup proof-easy-config-check-setup59,2510 (defmacro proof-easy-config proof-easy-config91,3835 generic/proof.el,809 (deflocal proof-buffer-type proof-buffer-type35,900 (defvar proof-shell-busy proof-shell-busy38,1013 (defvar proof-included-files-list proof-included-files-list43,1169 (defvar proof-script-buffer proof-script-buffer66,2185 (defvar proof-previous-script-buffer proof-previous-script-buffer70,2325 (defvar proof-shell-buffer proof-shell-buffer75,2579 (defvar proof-goals-buffer proof-goals-buffer78,2665 (defvar proof-response-buffer proof-response-buffer81,2720 (defvar proof-trace-buffer proof-trace-buffer84,2781 (defvar proof-thms-buffer proof-thms-buffer88,2935 (defvar proof-shell-error-or-interrupt-seen proof-shell-error-or-interrupt-seen92,3090 (defvar proof-shell-proof-completed proof-shell-proof-completed97,3315 (defvar proof-terminal-string proof-terminal-string109,3860 generic/proof-indent.el,475 (defun proof-indent-indent proof-indent-indent13,353 (defun proof-indent-offset proof-indent-offset22,619 (defun proof-indent-inner-p proof-indent-inner-p39,1219 (defun proof-indent-goto-prev proof-indent-goto-prev48,1526 (defun proof-indent-calculate proof-indent-calculate55,1859 (defun proof-indent-line proof-indent-line74,2575 (defun proof-indent-pad-eol proof-indent-pad-eol98,3376 (defun proof-indent-pad-eol-region proof-indent-pad-eol-region116,3970 generic/proof-menu.el,4166 (defvar proof-display-some-buffers-count proof-display-some-buffers-count19,467 (defun proof-display-some-buffers proof-display-some-buffers21,512 (defun proof-menu-define-keys proof-menu-define-keys80,2714 (define-key map map83,2862 (define-key map map84,2914 (define-key map map85,2965 (define-key map map86,3018 (define-key map map87,3072 (define-key map map88,3134 (define-key map map89,3194 (define-key map map90,3256 (define-key map map92,3377 (define-key map map93,3441 (define-key map map96,3619 (define-key map map97,3690 (define-key map map98,3744 (define-key map map99,3809 (define-key map map100,3883 (define-key map map103,4064 (define-key map map104,4130 (define-key map map106,4280 (define-key map map107,4350 (define-key map map108,4416 (define-key map map110,4531 (define-key map map111,4594 (define-key map map113,4679 (define-key map map120,5005 (define-key map map121,5064 (defun proof-menu-define-main proof-menu-define-main141,5654 (defun proof-menu-define-specific proof-menu-define-specific151,5855 (defun proof-assistant-menu-update proof-assistant-menu-update186,6872 (defvar proof-help-menuproof-help-menu200,7303 (defvar proof-show-hide-menuproof-show-hide-menu208,7581 (defvar proof-buffer-menuproof-buffer-menu217,7894 (defconst proof-quick-opts-menuproof-quick-opts-menu272,9886 (defun proof-quick-opts-vars proof-quick-opts-vars380,14317 (defun proof-quick-opts-changed-from-defaults-p proof-quick-opts-changed-from-defaults-p403,14999 (defun proof-quick-opts-changed-from-saved-p proof-quick-opts-changed-from-saved-p407,15104 (defun proof-quick-opts-save proof-quick-opts-save418,15456 (defun proof-quick-opts-reset proof-quick-opts-reset423,15624 (defconst proof-config-menuproof-config-menu435,15892 (defconst proof-advanced-menuproof-advanced-menu442,16071 (defvar proof-menu proof-menu458,16650 (defvar proof-main-menuproof-main-menu467,16934 (defvar proof-aux-menuproof-aux-menu477,17160 (defvar proof-menu-favourites proof-menu-favourites493,17482 (defun proof-menu-define-favourites-menu proof-menu-define-favourites-menu496,17589 (defmacro proof-defshortcut proof-defshortcut517,18260 (defmacro proof-definvisible proof-definvisible533,18915 (defun proof-def-favourite proof-def-favourite554,19740 (defvar proof-make-favourite-cmd-history proof-make-favourite-cmd-history577,20715 (defvar proof-make-favourite-menu-history proof-make-favourite-menu-history580,20800 (defun proof-save-favourites proof-save-favourites583,20886 (defun proof-del-favourite proof-del-favourite588,21034 (defun proof-read-favourite proof-read-favourite605,21595 (defun proof-add-favourite proof-add-favourite630,22398 (defvar proof-assistant-settings proof-assistant-settings657,23449 (defvar proof-menu-settings proof-menu-settings664,23812 (defun proof-menu-define-settings-menu proof-menu-define-settings-menu667,23886 (defun proof-menu-entry-name proof-menu-entry-name687,24630 (defun proof-menu-entry-for-setting proof-menu-entry-for-setting699,25102 (defun proof-settings-vars proof-settings-vars717,25592 (defun proof-settings-changed-from-defaults-p proof-settings-changed-from-defaults-p722,25769 (defun proof-settings-changed-from-saved-p proof-settings-changed-from-saved-p726,25875 (defun proof-settings-save proof-settings-save730,25978 (defun proof-settings-reset proof-settings-reset735,26145 (defun proof-defpacustom-fn proof-defpacustom-fn743,26391 (defmacro defpacustom defpacustom819,29275 (defun proof-assistant-invisible-command-ifposs proof-assistant-invisible-command-ifposs830,29916 (defun proof-maybe-askprefs proof-maybe-askprefs852,30891 (defun proof-assistant-settings-cmd proof-assistant-settings-cmd859,31095 (defun proof-assistant-format proof-assistant-format876,31755 (defvar proof-assistant-format-table proof-assistant-format-table900,32814 (defun proof-assistant-format-bool proof-assistant-format-bool908,33183 (defun proof-assistant-format-int proof-assistant-format-int911,33296 (defun proof-assistant-format-string proof-assistant-format-string914,33388 generic/proof-mmm.el,179 (defun proof-mmm-support-available proof-mmm-support-available25,909 (defun proof-mmm-set-global proof-mmm-set-global49,1757 (defun proof-mmm-enable proof-mmm-enable64,2298 generic/proof-script.el,8107 (defvar proof-last-theorem-dependencies proof-last-theorem-dependencies41,1046 (defvar proof-nesting-depth proof-nesting-depth45,1208 (defvar proof-element-counters proof-element-counters52,1439 (deflocal proof-active-buffer-fake-minor-mode proof-active-buffer-fake-minor-mode58,1579 (deflocal proof-script-buffer-file-name proof-script-buffer-file-name61,1705 (defun proof-next-element-count proof-next-element-count75,2229 (defun proof-element-id proof-element-id84,2556 (defun proof-next-element-id proof-next-element-id88,2725 (deflocal proof-script-last-entity proof-script-last-entity102,3041 (defun proof-script-find-next-entity proof-script-find-next-entity109,3321 (deflocal proof-locked-span proof-locked-span185,6063 (deflocal proof-queue-span proof-queue-span192,6329 (defun proof-span-read-only proof-span-read-only204,6843 (defun proof-strict-read-only proof-strict-read-only211,7100 (defsubst proof-set-queue-endpoints proof-set-queue-endpoints230,7987 (defsubst proof-set-locked-endpoints proof-set-locked-endpoints234,8128 (defsubst proof-detach-queue proof-detach-queue238,8272 (defsubst proof-detach-locked proof-detach-locked242,8404 (defsubst proof-set-queue-start proof-set-queue-start246,8540 (defsubst proof-set-locked-end proof-set-locked-end250,8666 (defsubst proof-set-queue-end proof-set-queue-end265,9213 (defun proof-init-segmentation proof-init-segmentation275,9469 (defun proof-restart-buffers proof-restart-buffers307,10840 (defun proof-script-buffers-with-spans proof-script-buffers-with-spans329,11762 (defun proof-script-remove-all-spans-and-deactivate proof-script-remove-all-spans-and-deactivate339,12118 (defun proof-script-clear-queue-spans proof-script-clear-queue-spans343,12306 (defun proof-unprocessed-begin proof-unprocessed-begin361,12847 (defun proof-script-end proof-script-end369,13101 (defun proof-queue-or-locked-end proof-queue-or-locked-end378,13402 (defun proof-locked-end proof-locked-end392,14065 (defun proof-locked-region-full-p proof-locked-region-full-p408,14435 (defun proof-locked-region-empty-p proof-locked-region-empty-p416,14692 (defun proof-only-whitespace-to-locked-region-p proof-only-whitespace-to-locked-region-p420,14842 (defun proof-in-locked-region-p proof-in-locked-region-p433,15478 (defun proof-goto-end-of-locked proof-goto-end-of-locked445,15741 (defun proof-goto-end-of-locked-if-pos-not-visible-in-window proof-goto-end-of-locked-if-pos-not-visible-in-window462,16500 (defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window473,16981 (defun proof-end-of-locked-visible-p proof-end-of-locked-visible-p487,17634 (defun proof-goto-end-of-queue-or-locked-if-not-visible proof-goto-end-of-queue-or-locked-if-not-visible496,18085 (defvar pg-idioms pg-idioms515,18735 (defvar pg-visibility-specs pg-visibility-specs518,18831 (deflocal pg-script-portions pg-script-portions523,19038 (defun pg-clear-script-portions pg-clear-script-portions526,19160 (defun pg-add-script-element pg-add-script-element544,19824 (defun pg-remove-script-element pg-remove-script-element547,19900 (defsubst pg-visname pg-visname555,20178 (defun pg-add-element pg-add-element559,20323 (defun pg-open-invisible-span pg-open-invisible-span593,21952 (defun pg-remove-element pg-remove-element604,22315 (defun pg-make-element-invisible pg-make-element-invisible611,22585 (defun pg-make-element-visible pg-make-element-visible617,22842 (defun pg-toggle-element-visibility pg-toggle-element-visibility622,23021 (defun pg-redisplay-for-gnuemacs pg-redisplay-for-gnuemacs630,23351 (defun pg-show-all-portions pg-show-all-portions637,23622 (defun pg-show-all-proofs pg-show-all-proofs655,24293 (defun pg-hide-all-proofs pg-hide-all-proofs660,24421 (defun pg-add-proof-element pg-add-proof-element665,24552 (defun pg-span-name pg-span-name679,25172 (defun pg-set-span-helphighlights pg-set-span-helphighlights700,25879 (defun proof-complete-buffer-atomic proof-complete-buffer-atomic725,26703 (defun proof-register-possibly-new-processed-file proof-register-possibly-new-processed-file766,28618 (defun proof-inform-prover-file-retracted proof-inform-prover-file-retracted817,30746 (defun proof-auto-retract-dependencies proof-auto-retract-dependencies836,31532 (defun proof-unregister-buffer-file-name proof-unregister-buffer-file-name890,34072 (defun proof-protected-process-or-retract proof-protected-process-or-retract936,35895 (defun proof-deactivate-scripting-auto proof-deactivate-scripting-auto963,37065 (defun proof-deactivate-scripting proof-deactivate-scripting972,37423 (defun proof-activate-scripting proof-activate-scripting1109,42828 (defun proof-toggle-active-scripting proof-toggle-active-scripting1237,48582 (defun proof-done-advancing proof-done-advancing1278,49943 (defun proof-done-advancing-comment proof-done-advancing-comment1363,53348 (defun proof-done-advancing-save proof-done-advancing-save1382,54090 (defun proof-make-goalsave proof-make-goalsave1475,57703 (defun proof-get-name-from-goal proof-get-name-from-goal1490,58446 (defun proof-done-advancing-autosave proof-done-advancing-autosave1509,59472 (defun proof-done-advancing-other proof-done-advancing-other1573,61989 (defun proof-segment-up-to-parser proof-segment-up-to-parser1601,62969 (defun proof-script-generic-parse-find-comment-end proof-script-generic-parse-find-comment-end1664,65045 (defun proof-script-generic-parse-cmdend proof-script-generic-parse-cmdend1673,65461 (defun proof-script-generic-parse-cmdstart proof-script-generic-parse-cmdstart1698,66356 (defun proof-script-generic-parse-sexp proof-script-generic-parse-sexp1761,69064 (defun proof-cmdstart-add-segment-for-cmd proof-cmdstart-add-segment-for-cmd1785,70000 (defun proof-segment-up-to-cmdstart proof-segment-up-to-cmdstart1837,72199 (defun proof-segment-up-to-cmdend proof-segment-up-to-cmdend1898,74559 (defun proof-semis-to-vanillas proof-semis-to-vanillas1969,77206 (defun proof-script-new-command-advance proof-script-new-command-advance2008,78532 (defun proof-script-next-command-advance proof-script-next-command-advance2050,80273 (defun proof-assert-until-point-interactive proof-assert-until-point-interactive2062,80714 (defun proof-assert-until-point proof-assert-until-point2088,81836 (defun proof-assert-next-commandproof-assert-next-command2141,84268 (defun proof-goto-point proof-goto-point2189,86531 (defun proof-insert-pbp-command proof-insert-pbp-command2206,87057 (defun proof-done-retracting proof-done-retracting2238,88130 (defun proof-setup-retract-action proof-setup-retract-action2265,89241 (defun proof-last-goal-or-goalsave proof-last-goal-or-goalsave2275,89724 (defun proof-retract-target proof-retract-target2299,90593 (defun proof-retract-until-point-interactive proof-retract-until-point-interactive2384,94234 (defun proof-retract-until-point proof-retract-until-point2392,94619 (define-derived-mode proof-mode proof-mode2437,96480 (defun proof-script-set-visited-file-name proof-script-set-visited-file-name2473,97966 (defun proof-script-set-buffer-hooks proof-script-set-buffer-hooks2497,98968 (defun proof-script-kill-buffer-fn proof-script-kill-buffer-fn2507,99464 (defun proof-config-done-related proof-config-done-related2551,101286 (defun proof-generic-goal-command-p proof-generic-goal-command-p2623,103854 (defun proof-generic-state-preserving-p proof-generic-state-preserving-p2627,104029 (defun proof-generic-count-undos proof-generic-count-undos2636,104546 (defun proof-generic-find-and-forget proof-generic-find-and-forget2665,105576 (defconst proof-script-important-settingsproof-script-important-settings2716,107401 (defun proof-config-done proof-config-done2729,107938 (defun proof-setup-parsing-mechanism proof-setup-parsing-mechanism2826,111486 (defun proof-setup-imenu proof-setup-imenu2870,113339 (defun proof-setup-func-menu proof-setup-func-menu2887,113944 generic/proof-shell.el,5296 (defvar proof-shell-last-output proof-shell-last-output19,464 (defvar proof-marker proof-marker63,1720 (defvar proof-action-list proof-action-list66,1817 (defvar proof-shell-silent proof-shell-silent74,1993 (defvar proof-shell-last-prompt proof-shell-last-prompt88,2476 (defvar proof-shell-last-output-kind proof-shell-last-output-kind93,2706 (defvar proof-shell-delayed-output proof-shell-delayed-output114,3528 (defvar proof-shell-delayed-output-kind proof-shell-delayed-output-kind117,3649 (defcustom proof-shell-active-scripting-indicatorproof-shell-active-scripting-indicator126,3852 (defun proof-shell-ready-prover proof-shell-ready-prover179,5328 (defun proof-shell-live-buffer proof-shell-live-buffer193,5868 (defun proof-shell-available-p proof-shell-available-p200,6103 (defun proof-grab-lock proof-grab-lock206,6326 (defun proof-release-lock proof-release-lock223,7043 (defcustom proof-shell-fiddle-frames proof-shell-fiddle-frames243,7599 (deflocal proof-eagerly-raise proof-eagerly-raise250,7840 (defun proof-shell-start proof-shell-start253,7946 (defvar proof-shell-kill-function-hooks proof-shell-kill-function-hooks445,15498 (defun proof-shell-kill-function proof-shell-kill-function448,15596 (defun proof-shell-clear-state proof-shell-clear-state539,19456 (defun proof-shell-exit proof-shell-exit554,19899 (defun proof-shell-bail-out proof-shell-bail-out566,20344 (defun proof-shell-restart proof-shell-restart575,20821 (defvar proof-shell-no-response-display proof-shell-no-response-display617,22205 (defvar proof-shell-urgent-message-marker proof-shell-urgent-message-marker620,22309 (defvar proof-shell-urgent-message-scanner proof-shell-urgent-message-scanner623,22430 (defun proof-shell-handle-output proof-shell-handle-output627,22557 (defun proof-shell-handle-delayed-output proof-shell-handle-delayed-output700,25880 (defvar proof-shell-no-error-display proof-shell-no-error-display735,27302 (defun proof-shell-handle-error proof-shell-handle-error741,27508 (defun proof-shell-handle-interrupt proof-shell-handle-interrupt759,28344 (defun proof-shell-error-or-interrupt-action proof-shell-error-or-interrupt-action773,28966 (defun proof-goals-pos proof-goals-pos800,30171 (defun proof-pbp-focus-on-first-goal proof-pbp-focus-on-first-goal805,30376 (defsubst proof-shell-string-match-safe proof-shell-string-match-safe817,30911 (defun proof-shell-process-output proof-shell-process-output822,31079 (defvar proof-shell-insert-space-fudge proof-shell-insert-space-fudge933,35719 (defun proof-shell-insert proof-shell-insert942,36028 (defun proof-shell-command-queue-item proof-shell-command-queue-item1016,38940 (defun proof-shell-set-silent proof-shell-set-silent1021,39097 (defun proof-shell-start-silent-item proof-shell-start-silent-item1027,39316 (defun proof-shell-clear-silent proof-shell-clear-silent1033,39508 (defun proof-shell-stop-silent-item proof-shell-stop-silent-item1039,39730 (defun proof-shell-should-be-silent proof-shell-should-be-silent1046,40002 (defun proof-append-alist proof-append-alist1059,40558 (defun proof-start-queue proof-start-queue1115,42685 (defun proof-extend-queue proof-extend-queue1126,43034 (defun proof-shell-exec-loop proof-shell-exec-loop1137,43415 (defun proof-shell-insert-loopback-cmd proof-shell-insert-loopback-cmd1202,46003 (defun proof-shell-message proof-shell-message1239,47711 (defun proof-shell-process-urgent-message proof-shell-process-urgent-message1245,47927 (defvar proof-shell-minibuffer-urgent-interactive-input-history proof-shell-minibuffer-urgent-interactive-input-history1453,56775 (defun proof-shell-minibuffer-urgent-interactive-input proof-shell-minibuffer-urgent-interactive-input1455,56845 (defun proof-shell-process-urgent-messages proof-shell-process-urgent-messages1467,57215 (defun proof-shell-filter proof-shell-filter1539,60385 (defun proof-shell-filter-process-output proof-shell-filter-process-output1692,66722 (defvar pg-last-tracing-output-time pg-last-tracing-output-time1745,68776 (defvar pg-tracing-slow-mode pg-tracing-slow-mode1748,68882 (defconst pg-slow-mode-duration pg-slow-mode-duration1751,68971 (defconst pg-fast-tracing-mode-threshold pg-fast-tracing-mode-threshold1754,69053 (defvar pg-tracing-cleanup-timer pg-tracing-cleanup-timer1757,69181 (defun pg-tracing-tight-loop pg-tracing-tight-loop1759,69220 (defun pg-finish-tracing-display pg-finish-tracing-display1802,70938 (defun proof-shell-dont-show-annotations proof-shell-dont-show-annotations1815,71244 (defun proof-shell-show-annotations proof-shell-show-annotations1831,71779 (defun proof-shell-wait proof-shell-wait1852,72276 (defun proof-done-invisible proof-done-invisible1872,73186 (defun proof-shell-invisible-command proof-shell-invisible-command1915,74909 (defun proof-shell-invisible-cmd-get-result proof-shell-invisible-cmd-get-result1948,76159 (defun proof-shell-invisible-command-invisible-result proof-shell-invisible-command-invisible-result1965,76840 (define-derived-mode proof-shell-mode proof-shell-mode1985,77344 (defconst proof-shell-important-settingsproof-shell-important-settings2053,79897 (defun proof-shell-config-done proof-shell-config-done2058,79997 generic/proof-site.el,1030 (defgroup proof-general proof-general20,594 (defgroup proof-general-internals proof-general-internals33,1010 (defun proof-home-directory-fn proof-home-directory-fn42,1203 (defcustom proof-home-directoryproof-home-directory53,1573 (defcustom proof-images-directoryproof-images-directory62,1939 (defcustom proof-info-directoryproof-info-directory68,2140 (defcustom proof-assistant-tableproof-assistant-table97,3389 (defun proof-string-to-list proof-string-to-list163,5571 (defcustom proof-assistants proof-assistants179,6062 (defun proof-ready-for-assistant proof-ready-for-assistant215,7475 (defconst proof-general-version proof-general-version328,11684 (defconst proof-general-short-version proof-general-short-version331,11825 (defcustom proof-assistant-cusgrp proof-assistant-cusgrp348,12407 (defcustom proof-assistant-internals-cusgrp proof-assistant-internals-cusgrp356,12710 (defcustom proof-assistant proof-assistant364,13022 (defcustom proof-assistant-symbol proof-assistant-symbol372,13291 generic/proof-splash.el,1149 (defcustom proof-splash-enable proof-splash-enable14,379 (defcustom proof-splash-time proof-splash-time19,531 (defcustom proof-splash-contentsproof-splash-contents27,816 (defconst proof-splash-startup-msg proof-splash-startup-msg56,1895 (defconst proof-splash-welcome proof-splash-welcome65,2274 (defun proof-get-image proof-get-image84,2838 (defvar proof-splash-timeout-conf proof-splash-timeout-conf136,4662 (defun proof-splash-centre-spaces proof-splash-centre-spaces139,4775 (defun proof-splash-remove-screen proof-splash-remove-screen167,5944 (defun proof-splash-remove-buffer proof-splash-remove-buffer188,6693 (defvar proof-splash-seen proof-splash-seen204,7357 (defun proof-splash-display-screen proof-splash-display-screen208,7474 (defun proof-splash-message proof-splash-message283,10633 (defun proof-splash-timeout-waiter proof-splash-timeout-waiter293,10996 (defvar proof-splash-old-frame-title-format proof-splash-old-frame-title-format310,11735 (defun proof-splash-set-frame-titles proof-splash-set-frame-titles312,11785 (defun proof-splash-unset-frame-titles proof-splash-unset-frame-titles321,12101 generic/proof-syntax.el,1297 (defun proof-ids-to-regexp proof-ids-to-regexp16,445 (defun proof-anchor-regexp proof-anchor-regexp22,701 (defconst proof-no-regexpproof-no-regexp26,803 (defun proof-regexp-alt proof-regexp-alt31,898 (defun proof-regexp-region proof-regexp-region40,1184 (defun proof-re-search-forward-region proof-re-search-forward-region49,1607 (defun proof-re-search-forward proof-re-search-forward62,2102 (defun proof-re-search-backward proof-re-search-backward68,2363 (defun proof-string-match proof-string-match74,2627 (defun proof-string-match-safe proof-string-match-safe80,2859 (defun proof-stringfn-match proof-stringfn-match84,3064 (defun proof-looking-at proof-looking-at91,3324 (defun proof-looking-at-safe proof-looking-at-safe97,3514 (defun proof-looking-at-syntactic-context proof-looking-at-syntactic-context101,3654 (defun proof-replace-string proof-replace-string113,3986 (defun proof-replace-regexp proof-replace-regexp118,4171 (defvar proof-id proof-id126,4384 (defun proof-ids proof-ids132,4604 (defun proof-zap-commas proof-zap-commas145,5165 (defun proof-format proof-format163,5728 (defun proof-format-filename proof-format-filename182,6367 (defun proof-insert proof-insert231,7845 (defun proof-splice-separator proof-splice-separator267,8854 generic/proof-system.el,0 generic/proof-toolbar.el,3888 (defun proof-toolbar-function proof-toolbar-function57,1920 (defun proof-toolbar-icon proof-toolbar-icon60,2017 (defun proof-toolbar-enabler proof-toolbar-enabler63,2118 (defun proof-toolbar-function-with-enabler proof-toolbar-function-with-enabler66,2226 (defun proof-toolbar-make-icon proof-toolbar-make-icon73,2399 (defun proof-toolbar-make-toolbar-item proof-toolbar-make-toolbar-item91,2999 (defvar proof-toolbar proof-toolbar130,4380 (deflocal proof-toolbar-itimer proof-toolbar-itimer134,4509 (defun proof-toolbar-setup proof-toolbar-setup138,4619 (defun proof-toolbar-build proof-toolbar-build183,6235 (defalias 'proof-toolbar-enable proof-toolbar-enable257,8796 (defun proof-toolbar-setup-refresh proof-toolbar-setup-refresh266,9035 (defun proof-toolbar-disable-refresh proof-toolbar-disable-refresh287,9805 (deflocal proof-toolbar-refresh-flag proof-toolbar-refresh-flag294,10127 (defun proof-toolbar-refresh proof-toolbar-refresh300,10398 (defvar proof-toolbar-enablersproof-toolbar-enablers304,10543 (defvar proof-toolbar-enablers-last-stateproof-toolbar-enablers-last-state310,10719 (defun proof-toolbar-really-refresh proof-toolbar-really-refresh314,10810 (defun proof-toolbar-undo-enable-p proof-toolbar-undo-enable-p367,12640 (defalias 'proof-toolbar-undo proof-toolbar-undo372,12788 (defun proof-toolbar-delete-enable-p proof-toolbar-delete-enable-p378,12907 (defalias 'proof-toolbar-delete proof-toolbar-delete384,13081 (defun proof-toolbar-lockedend-enable-p proof-toolbar-lockedend-enable-p391,13217 (defalias 'proof-toolbar-lockedend proof-toolbar-lockedend394,13267 (defun proof-toolbar-next-enable-p proof-toolbar-next-enable-p403,13355 (defalias 'proof-toolbar-next proof-toolbar-next407,13462 (defun proof-toolbar-goto-enable-p proof-toolbar-goto-enable-p414,13556 (defalias 'proof-toolbar-goto proof-toolbar-goto417,13629 (defun proof-toolbar-retract-enable-p proof-toolbar-retract-enable-p424,13705 (defalias 'proof-toolbar-retract proof-toolbar-retract428,13816 (defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p435,13895 (defalias 'proof-toolbar-use proof-toolbar-use436,13963 (defun proof-toolbar-restart-enable-p proof-toolbar-restart-enable-p442,14041 (defalias 'proof-toolbar-restart proof-toolbar-restart447,14202 (defun proof-toolbar-goal-enable-p proof-toolbar-goal-enable-p453,14280 (defalias 'proof-toolbar-goal proof-toolbar-goal460,14513 (defun proof-toolbar-qed-enable-p proof-toolbar-qed-enable-p467,14585 (defalias 'proof-toolbar-qed proof-toolbar-qed473,14737 (defun proof-toolbar-state-enable-p proof-toolbar-state-enable-p479,14809 (defalias 'proof-toolbar-state proof-toolbar-state482,14880 (defun proof-toolbar-context-enable-p proof-toolbar-context-enable-p488,14949 (defalias 'proof-toolbar-context proof-toolbar-context491,15022 (defun proof-toolbar-info-enable-p proof-toolbar-info-enable-p499,15182 (defalias 'proof-toolbar-info proof-toolbar-info502,15226 (defun proof-toolbar-command-enable-p proof-toolbar-command-enable-p508,15295 (defalias 'proof-toolbar-command proof-toolbar-command511,15366 (defun proof-toolbar-help-enable-p proof-toolbar-help-enable-p517,15446 (defun proof-toolbar-help proof-toolbar-help520,15491 (defun proof-toolbar-find-enable-p proof-toolbar-find-enable-p528,15585 (defalias 'proof-toolbar-find proof-toolbar-find531,15654 (defun proof-toolbar-visibility-enable-p proof-toolbar-visibility-enable-p537,15752 (defalias 'proof-toolbar-visibility proof-toolbar-visibility540,15852 (defun proof-toolbar-interrupt-enable-p proof-toolbar-interrupt-enable-p546,15940 (defalias 'proof-toolbar-interrupt proof-toolbar-interrupt549,16004 (defun proof-toolbar-make-menu-item proof-toolbar-make-menu-item558,16193 (defconst proof-toolbar-scripting-menuproof-toolbar-scripting-menu580,16881 generic/proof-utils.el,3150 (defmacro deflocal deflocal18,471 (defmacro proof-with-current-buffer-if-exists proof-with-current-buffer-if-exists25,709 (defmacro proof-with-script-buffer proof-with-script-buffer34,1086 (defmacro proof-map-buffers proof-map-buffers45,1473 (defmacro proof-sym proof-sym50,1658 (defun proof-try-require proof-try-require55,1819 (defun proof-save-some-buffers proof-save-some-buffers68,2147 (defun proof-set-value proof-set-value92,2838 (defun proof-ass-symv proof-ass-symv152,5015 (defmacro proof-ass-sym proof-ass-sym157,5202 (defun proof-defpgcustom-fn proof-defpgcustom-fn161,5341 (defun undefpgcustom undefpgcustom186,6425 (defmacro defpgcustom defpgcustom192,6649 (defmacro proof-ass proof-ass201,7066 (defun proof-defpgdefault-fn proof-defpgdefault-fn206,7242 (defmacro defpgdefault defpgdefault220,7701 (defmacro defpgfun defpgfun231,8063 (defun proof-file-truename proof-file-truename246,8357 (defun proof-file-to-buffer proof-file-to-buffer250,8540 (defun proof-files-to-buffers proof-files-to-buffers261,8869 (defun proof-buffers-in-mode proof-buffers-in-mode268,9152 (defun pg-save-from-death pg-save-from-death282,9603 (defun proof-define-keys proof-define-keys301,10213 (deflocal proof-font-lock-keywords proof-font-lock-keywords330,11214 (deflocal proof-font-lock-keywords-case-fold-search proof-font-lock-keywords-case-fold-search336,11479 (defun proof-font-lock-configure-defaults proof-font-lock-configure-defaults339,11602 (defun proof-font-lock-clear-font-lock-vars proof-font-lock-clear-font-lock-vars387,13915 (defun proof-font-lock-set-font-lock-vars proof-font-lock-set-font-lock-vars398,14288 (defun proof-fontify-region proof-fontify-region405,14501 (defconst pg-special-char-regexp pg-special-char-regexp464,16730 (defun pg-remove-specials pg-remove-specials468,16842 (defun proof-fontify-buffer proof-fontify-buffer482,17267 (defun proof-warn-if-unset proof-warn-if-unset495,17508 (defun proof-get-window-for-buffer proof-get-window-for-buffer500,17726 (defun proof-display-and-keep-buffer proof-display-and-keep-buffer537,19364 (defun proof-clean-buffer proof-clean-buffer569,20673 (defun proof-message proof-message583,21210 (defun proof-warning proof-warning588,21423 (defun pg-internal-warning pg-internal-warning594,21705 (defun proof-debug proof-debug602,22024 (defun proof-switch-to-buffer proof-switch-to-buffer617,22707 (defun proof-resize-window-tofit proof-resize-window-tofit650,24399 (defun proof-submit-bug-report proof-submit-bug-report750,28411 (defun proof-deftoggle-fn proof-deftoggle-fn775,29277 (defmacro proof-deftoggle proof-deftoggle790,29932 (defun proof-defintset-fn proof-defintset-fn797,30306 (defmacro proof-defintset proof-defintset811,30961 (defun proof-defstringset-fn proof-defstringset-fn818,31338 (defmacro proof-defstringset proof-defstringset831,31965 (defun pg-custom-save-vars pg-custom-save-vars845,32430 (defun pg-custom-reset-vars pg-custom-reset-vars863,33156 (defun proof-locate-executable proof-locate-executable876,33493 (defconst proof-extra-flsproof-extra-fls905,34674 generic/proof-x-symbol.el,960 (defvar proof-x-symbol-initialized proof-x-symbol-initialized54,2151 (defun proof-x-symbol-tokenlang-file proof-x-symbol-tokenlang-file57,2246 (defun proof-x-symbol-support-maybe-available proof-x-symbol-support-maybe-available63,2428 (defun proof-x-symbol-initialize proof-x-symbol-initialize83,3173 (defun proof-x-symbol-enable proof-x-symbol-enable178,7036 (defun proof-x-symbol-refresh-output-buffers proof-x-symbol-refresh-output-buffers208,8353 (defun proof-x-symbol-mode-associated-buffers proof-x-symbol-mode-associated-buffers223,9107 (defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region245,9811 (defun proof-x-symbol-encode-shell-input proof-x-symbol-encode-shell-input247,9877 (defun proof-x-symbol-set-language proof-x-symbol-set-language264,10468 (defun proof-x-symbol-shell-config proof-x-symbol-shell-config269,10639 (defun proof-x-symbol-config-output-buffer proof-x-symbol-config-output-buffer317,12806 hol98/hol98.el,0 hol98/x-symbol-hol98.el,0 isa/interface-setup.el,0 isa/isabelle-system.el,3268 (defconst isa-running-isar isa-running-isar17,537 (defgroup isabelle isabelle23,719 (defcustom isabelle-web-pageisabelle-web-page27,848 (defcustom isa-isatool-commandisa-isatool-command38,1143 (defvar isatool-not-found isatool-not-found65,2088 (defun isa-set-isatool-command isa-set-isatool-command68,2201 (defun isa-shell-command-to-string isa-shell-command-to-string88,2985 (defun isa-getenv isa-getenv94,3209 (defcustom isabelle-program-name isabelle-program-name113,3866 (defvar isabelle-prog-name isabelle-prog-name139,4814 (defun isabelle-command-line isabelle-command-line142,4941 (defun isabelle-choose-logic isabelle-choose-logic165,5849 (defun isa-tool-list-logics isa-tool-list-logics187,6821 (defun isa-view-doc isa-view-doc194,7059 (defvar isabelle-version-string isabelle-version-string201,7283 (defun isa-version isa-version203,7324 (defconst isa-supports-pgip isa-supports-pgip216,7807 (defun isa-tool-list-docs isa-tool-list-docs224,8037 (defun isa-quit isa-quit242,8759 (defconst isabelle-verbatim-regexp isabelle-verbatim-regexp249,8954 (defun isabelle-verbatim isabelle-verbatim252,9095 (defcustom isabelle-refresh-logics isabelle-refresh-logics268,9686 (defcustom isabelle-logics-available isabelle-logics-available276,10013 (defcustom isabelle-chosen-logic isabelle-chosen-logic284,10313 (defconst isabelle-docs-menu isabelle-docs-menu297,10781 (defun isabelle-logics-menu-calculate isabelle-logics-menu-calculate307,11174 (defvar isabelle-time-to-refresh-logics isabelle-time-to-refresh-logics323,11683 (defun isabelle-logics-menu-refresh isabelle-logics-menu-refresh326,11776 (defun isabelle-logics-menu-filter isabelle-logics-menu-filter343,12475 (defun isabelle-menu-bar-update-logics isabelle-menu-bar-update-logics349,12685 (defvar isabelle-logics-menu-entries isabelle-logics-menu-entries360,13041 (defvar isabelle-logics-menu isabelle-logics-menu362,13113 (defun isabelle-load-isar-keywords isabelle-load-isar-keywords375,13731 (defpacustom show-types show-types402,14686 (defpacustom show-sorts show-sorts407,14802 (defpacustom show-consts show-consts412,14918 (defpacustom long-names long-names417,15052 (defpacustom eta-contract eta-contract422,15184 (defpacustom trace-simplifier trace-simplifier427,15325 (defpacustom trace-rules trace-rules432,15457 (defpacustom quick-and-dirty quick-and-dirty437,15589 (defpacustom full-proofs full-proofs442,15725 (defpacustom global-timing global-timing448,16034 (defpacustom theorem-dependencies theorem-dependencies454,16192 (defpacustom goals-limit goals-limit460,16457 (defpacustom prems-limit prems-limit465,16596 (defpacustom print-depth print-depth470,16756 (defpgdefault menu-entriesmenu-entries482,17045 (defpgdefault help-menu-entries help-menu-entries489,17207 (defpgdefault x-symbol-language x-symbol-language497,17401 (defun isabelle-convert-idmarkup-to-subterm isabelle-convert-idmarkup-to-subterm520,18016 (defun isabelle-create-span-menu isabelle-create-span-menu545,19055 (defun isabelle-xml-sml-escapes isabelle-xml-sml-escapes562,19549 (defun isabelle-process-pgip isabelle-process-pgip565,19650 (defun isabelle-parse-syntax-dump isabelle-parse-syntax-dump582,20236 isa/isa.el,2283 (defcustom isa-outline-regexpisa-outline-regexp43,1354 (defcustom isa-outline-heading-end-regexp isa-outline-heading-end-regexp50,1591 (defvar isa-shell-outline-regexp isa-shell-outline-regexp55,1743 (defvar isa-shell-outline-heading-end-regexp isa-shell-outline-heading-end-regexp56,1805 (defun isa-mode-config-set-variables isa-mode-config-set-variables59,1857 (defun isa-shell-mode-config-set-variables isa-shell-mode-config-set-variables141,5266 (defun isa-update-thy-only isa-update-thy-only283,11186 (defun isa-shell-update-thy isa-shell-update-thy295,11694 (defun isa-remove-file isa-remove-file320,12897 (defun isa-shell-compute-new-files-list isa-shell-compute-new-files-list330,13215 (define-derived-mode isa-shell-mode isa-shell-mode346,13727 (define-derived-mode isa-response-mode isa-response-mode351,13852 (define-derived-mode isa-goals-mode isa-goals-mode356,14021 (define-derived-mode isa-proofscript-mode isa-proofscript-mode361,14178 (defun isa-mode isa-mode370,14359 (define-key map map414,15899 (define-key map map415,15949 (defun isa-process-thy-file isa-process-thy-file419,16106 (defcustom isa-retract-thy-file-command isa-retract-thy-file-command425,16315 (defun isa-retract-thy-file isa-retract-thy-file431,16552 (defgroup thy thy447,17181 (defun isa-splice-separator isa-splice-separator459,17511 (defun isa-file-name-cons-extension isa-file-name-cons-extension468,17763 (defun isa-format isa-format475,18029 (define-key isa-proofscript-mode-map isa-proofscript-mode-map487,18404 (defcustom isa-not-undoable-commands-regexpisa-not-undoable-commands-regexp497,18537 (defun isa-count-undos isa-count-undos504,18790 (defun isa-goal-command-p isa-goal-command-p534,19955 (defun isa-find-and-forget isa-find-and-forget547,20600 (defun isa-state-preserving-p isa-state-preserving-p550,20655 (defun isa-pre-shell-start isa-pre-shell-start559,21023 (defun isa-mode-config isa-mode-config566,21300 (defun isa-shell-mode-config isa-shell-mode-config594,22443 (defun isa-response-mode-config isa-response-mode-config601,22692 (defun isa-goals-mode-config isa-goals-mode-config606,22853 (defun isa-preprocessing isa-preprocessing614,23177 (defpgdefault completion-tablecompletion-table628,23681 isa/isa-syntax.el,3046 (defun isa-init-syntax-table isa-init-syntax-table14,312 (defun isa-init-output-syntax-table isa-init-output-syntax-table34,960 (defgroup isa-syntax isa-syntax71,2172 (defcustom isa-keywords-defnisa-keywords-defn75,2274 (defcustom isa-keywords-goalisa-keywords-goal82,2469 (defcustom isa-keywords-saveisa-keywords-save88,2676 (defcustom isa-keywords-commandsisa-keywords-commands97,2968 (defcustom isa-keywords-smlisa-keywords-sml109,3357 (defcustom isa-keyword-symbolsisa-keyword-symbols119,3826 (defcustom isa-sml-names-keywordsisa-sml-names-keywords125,4021 (defcustom isa-sml-typenames-keywordsisa-sml-typenames-keywords131,4194 (defconst isa-keywordsisa-keywords140,4490 (defconst isa-keywords-proof-commandsisa-keywords-proof-commands146,4671 (defconst isa-tacticalsisa-tacticals151,4865 (defconst isa-id isa-id159,5132 (defconst isa-idx isa-idx160,5181 (defconst isa-ids isa-ids162,5236 (defconst isa-string isa-string165,5347 (defcustom isa-save-command-regexpisa-save-command-regexp167,5406 (defconst isa-save-with-hole-regexpisa-save-with-hole-regexp181,5810 (defcustom isa-goal-command-regexpisa-goal-command-regexp185,5945 (defconst isa-string-regexpisa-string-regexp197,6329 (defconst isa-goal-with-hole-regexpisa-goal-with-hole-regexp201,6460 (defconst isa-proof-command-regexpisa-proof-command-regexp209,6702 (defface isabelle-class-name-faceisabelle-class-name-face216,6913 (defface isabelle-tfree-name-faceisabelle-tfree-name-face226,7198 (defface isabelle-tvar-name-faceisabelle-tvar-name-face236,7485 (defface isabelle-free-name-faceisabelle-free-name-face246,7775 (defface isabelle-bound-name-faceisabelle-bound-name-face256,8061 (defface isabelle-var-name-faceisabelle-var-name-face266,8350 (defface isabelle-sml-symbol-faceisabelle-sml-symbol-face277,8687 (defconst isabelle-class-name-face isabelle-class-name-face287,9063 (defconst isabelle-tfree-name-face isabelle-tfree-name-face288,9125 (defconst isabelle-tvar-name-face isabelle-tvar-name-face289,9187 (defconst isabelle-free-name-face isabelle-free-name-face290,9247 (defconst isabelle-bound-name-face isabelle-bound-name-face291,9307 (defconst isabelle-var-name-face isabelle-var-name-face292,9369 (defconst isabelle-sml-symbol-face isabelle-sml-symbol-face293,9427 (defconst isa-sml-function-var-names-regexp isa-sml-function-var-names-regexp296,9555 (defconst isa-sml-type-names-regexp isa-sml-type-names-regexp301,9815 (defvar isa-font-lock-keywords-1isa-font-lock-keywords-1305,9983 (defvar isa-output-font-lock-keywords-1isa-output-font-lock-keywords-1315,10540 (defvar isa-goals-font-lock-keywords isa-goals-font-lock-keywords327,11111 (defconst isa-indent-any-regexpisa-indent-any-regexp341,11386 (defconst isa-indent-inner-regexpisa-indent-inner-regexp343,11489 (defconst isa-indent-enclose-regexpisa-indent-enclose-regexp345,11559 (defconst isa-indent-open-regexpisa-indent-open-regexp347,11638 (defconst isa-indent-close-regexpisa-indent-close-regexp349,11740 isa/thy-mode.el,2895 (defcustom thy-heading-indent thy-heading-indent27,816 (defcustom thy-indent-level thy-indent-level32,920 (defcustom thy-indent-strings thy-indent-strings37,1047 (defcustom thy-use-sml-mode thy-use-sml-mode44,1272 (defcustom thy-sectionsthy-sections55,1680 (defcustom thy-id-headerthy-id-header108,3357 (defcustom thy-templatethy-template120,3657 (defvar thy-mode-map thy-mode-map145,4085 (defvar thy-mode-syntax-table thy-mode-syntax-table147,4112 (defun thy-add-menus thy-add-menus182,5672 (defun thy-mode thy-mode220,7068 (defun thy-mode-quiet thy-mode-quiet275,8827 (defun thy-proofgeneral-send-string thy-proofgeneral-send-string355,11587 (defun isa-sml-hook isa-sml-hook434,14194 (defun isa-sml-mode isa-sml-mode448,14789 (defcustom isa-ml-file-extension isa-ml-file-extension453,14921 (defun thy-find-other-file thy-find-other-file458,15043 (defvar thy-minor-sml-mode-map thy-minor-sml-mode-map481,15925 (defun thy-install-sml-mode thy-install-sml-mode483,15962 (defun thy-minor-sml-mode thy-minor-sml-mode492,16348 (defun thy-do-sml-indent thy-do-sml-indent510,16998 (defun thy-insert-name thy-insert-name520,17395 (defun thy-insert-class thy-insert-class526,17593 (defun thy-insert-default-sort thy-insert-default-sort536,17865 (defun thy-insert-type thy-insert-type544,18037 (defun thy-insert-arity thy-insert-arity567,18607 (defun thy-insert-const thy-insert-const580,18982 (defun thy-insert-rule thy-insert-rule592,19371 (defun thy-insert-template thy-insert-template601,19553 (defun isa-read-idlist isa-read-idlist633,20432 (defun isa-read-id isa-read-id642,20719 (defun isa-read-string isa-read-string650,20948 (defun isa-read-num isa-read-num658,21185 (defun thy-read-thy-name thy-read-thy-name669,21477 (defun thy-read-logic-image thy-read-logic-image678,21779 (defun thy-insert-header thy-insert-header688,22043 (defun thy-insert-id-header thy-insert-id-header706,22608 (defun thy-check-mode thy-check-mode718,22967 (defconst thy-headings-regexpthy-headings-regexp723,23072 (defvar thy-mode-font-lock-keywordsthy-mode-font-lock-keywords733,23331 (defun thy-goto-next-section thy-goto-next-section755,24091 (defun thy-goto-prev-section thy-goto-prev-section783,25068 (defun thy-goto-top-of-section thy-goto-top-of-section790,25381 (defun thy-current-section thy-current-section797,25578 (defun thy-kill-line thy-kill-line815,26041 (defun thy-indent-line thy-indent-line877,28125 (defun thy-calculate-indentation thy-calculate-indentation904,29159 (defun thy-long-comment-string-indentation thy-long-comment-string-indentation924,29818 (defun thy-string-indentation thy-string-indentation959,30802 (defun thy-indentation-for thy-indentation-for978,31452 (defun thy-string-start thy-string-start984,31611 (defun thy-comment-or-string-start thy-comment-or-string-start998,32148 isa/x-symbol-isabelle.el,3169 (defvar x-symbol-isabelle-required-fonts x-symbol-isabelle-required-fonts20,624 (defvar x-symbol-isabelle-name x-symbol-isabelle-name28,1028 (defvar x-symbol-isabelle-modeline-name x-symbol-isabelle-modeline-name29,1078 (defcustom x-symbol-isabelle-header-groups-alist x-symbol-isabelle-header-groups-alist31,1126 (defcustom x-symbol-isabelle-electric-ignore x-symbol-isabelle-electric-ignore38,1354 (defvar x-symbol-isabelle-required-fonts x-symbol-isabelle-required-fonts46,1610 (defvar x-symbol-isabelle-extra-menu-items x-symbol-isabelle-extra-menu-items49,1719 (defvar x-symbol-isabelle-token-grammarx-symbol-isabelle-token-grammar53,1817 (defun x-symbol-isabelle-token-list x-symbol-isabelle-token-list60,2023 (defvar x-symbol-isabelle-user-table x-symbol-isabelle-user-table63,2112 (defvar x-symbol-isabelle-generated-data x-symbol-isabelle-generated-data66,2233 (defvar x-symbol-isabelle-master-directory x-symbol-isabelle-master-directory74,2476 (defvar x-symbol-isabelle-image-searchpath x-symbol-isabelle-image-searchpath75,2529 (defvar x-symbol-isabelle-image-cached-dirs x-symbol-isabelle-image-cached-dirs76,2581 (defvar x-symbol-isabelle-image-file-truename-alist x-symbol-isabelle-image-file-truename-alist77,2651 (defvar x-symbol-isabelle-image-keywords x-symbol-isabelle-image-keywords78,2708 (defcustom x-symbol-isabelle-subscript-matcher x-symbol-isabelle-subscript-matcher88,3052 (defcustom x-symbol-isabelle-font-lock-regexp x-symbol-isabelle-font-lock-regexp94,3299 (defcustom x-symbol-isabelle-font-lock-limit-regexp x-symbol-isabelle-font-lock-limit-regexp99,3483 (defcustom x-symbol-isabelle-font-lock-contents-regexp x-symbol-isabelle-font-lock-contents-regexp105,3701 (defcustom x-symbol-isabelle-single-char-regexp x-symbol-isabelle-single-char-regexp115,4078 (defun x-symbol-isabelle-subscript-matcher x-symbol-isabelle-subscript-matcher121,4288 (defun isabelle-match-subscript isabelle-match-subscript155,5963 (defvar x-symbol-isabelle-font-lock-keywordsx-symbol-isabelle-font-lock-keywords164,6358 (defvar x-symbol-isabelle-font-lock-allowed-faces x-symbol-isabelle-font-lock-allowed-faces171,6626 (defcustom x-symbol-isabelle-class-alistx-symbol-isabelle-class-alist178,6858 (defcustom x-symbol-isabelle-class-face-alist x-symbol-isabelle-class-face-alist189,7283 (defvar x-symbol-isabelle-case-insensitive x-symbol-isabelle-case-insensitive204,7811 (defvar x-symbol-isabelle-token-shape x-symbol-isabelle-token-shape205,7859 (defvar x-symbol-isabelle-input-token-ignore x-symbol-isabelle-input-token-ignore206,7902 (defvar x-symbol-isabelle-token-list x-symbol-isabelle-token-list207,7952 (defvar x-symbol-isabelle-symbol-table x-symbol-isabelle-symbol-table209,8001 (defvar x-symbol-isabelle-xsymbol-table x-symbol-isabelle-xsymbol-table309,10737 (defun x-symbol-isabelle-prepare-table x-symbol-isabelle-prepare-table454,15139 (defvar x-symbol-isabelle-tablex-symbol-isabelle-table466,15550 (defcustom x-symbol-isabelle-auto-stylex-symbol-isabelle-auto-style480,15903 (defcustom x-symbol-isabelle-auto-coding-alist x-symbol-isabelle-auto-coding-alist494,16413 isa/x-symbol-isa.el,0 isar/isar-autotest.el,0 isar/isar.el,1927 (defcustom isar-keywords-name isar-keywords-name28,631 (defpgdefault completion-table completion-table45,1155 (defcustom isar-web-pageisar-web-page47,1208 (defun isar-detect-header isar-detect-header65,1572 (defun isar-strip-terminators isar-strip-terminators100,2835 (defun isar-markup-ml isar-markup-ml113,3206 (defun isar-mode-config-set-variables isar-mode-config-set-variables118,3341 (defun isar-shell-mode-config-set-variables isar-shell-mode-config-set-variables182,6172 (defun isar-remove-file isar-remove-file296,10939 (defun isar-shell-compute-new-files-list isar-shell-compute-new-files-list306,11302 (defun isar-activate-scripting isar-activate-scripting317,11768 (define-derived-mode isar-shell-mode isar-shell-mode326,11938 (define-derived-mode isar-response-mode isar-response-mode331,12061 (define-derived-mode isar-goals-mode isar-goals-mode336,12243 (define-derived-mode isar-mode isar-mode341,12418 (define-key (proof-ass proof-ass363,12999 (defpgdefault menu-entriesmenu-entries398,14550 (defun isar-count-undos isar-count-undos428,15872 (defun isar-find-and-forget isar-find-and-forget454,16973 (defun isar-goal-command-p isar-goal-command-p501,18818 (defun isar-global-save-command-p isar-global-save-command-p505,18950 (defvar isar-current-goal isar-current-goal526,19787 (defun isar-state-preserving-p isar-state-preserving-p529,19853 (defvar isar-shell-current-line-width isar-shell-current-line-width552,20887 (defun isar-shell-adjust-line-width isar-shell-adjust-line-width558,21105 (defun isar-pre-shell-start isar-pre-shell-start578,21988 (defun isar-preprocessing isar-preprocessing590,22324 (defun isar-mode-config isar-mode-config613,23535 (defun isar-shell-mode-config isar-shell-mode-config625,24105 (defun isar-response-mode-config isar-response-mode-config636,24475 (defun isar-goals-mode-config isar-goals-mode-config645,24732 isar/isar-keywords.el,1650 (defconst isar-keywords-majorisar-keywords-major14,378 (defconst isar-keywords-minorisar-keywords-minor169,2840 (defconst isar-keywords-controlisar-keywords-control207,3351 (defconst isar-keywords-diagisar-keywords-diag225,3768 (defconst isar-keywords-theory-beginisar-keywords-theory-begin268,4490 (defconst isar-keywords-theory-switchisar-keywords-theory-switch271,4543 (defconst isar-keywords-theory-endisar-keywords-theory-end274,4598 (defconst isar-keywords-theory-headingisar-keywords-theory-heading277,4646 (defconst isar-keywords-theory-declisar-keywords-theory-decl283,4753 (defconst isar-keywords-theory-scriptisar-keywords-theory-script326,5463 (defconst isar-keywords-theory-goalisar-keywords-theory-goal330,5540 (defconst isar-keywords-qedisar-keywords-qed337,5650 (defconst isar-keywords-qed-blockisar-keywords-qed-block344,5736 (defconst isar-keywords-qed-globalisar-keywords-qed-global347,5783 (defconst isar-keywords-proof-headingisar-keywords-proof-heading350,5832 (defconst isar-keywords-proof-goalisar-keywords-proof-goal355,5915 (defconst isar-keywords-proof-blockisar-keywords-proof-block361,5998 (defconst isar-keywords-proof-openisar-keywords-proof-open365,6060 (defconst isar-keywords-proof-closeisar-keywords-proof-close368,6106 (defconst isar-keywords-proof-chainisar-keywords-proof-chain371,6153 (defconst isar-keywords-proof-declisar-keywords-proof-decl378,6256 (defconst isar-keywords-proof-asmisar-keywords-proof-asm386,6365 (defconst isar-keywords-proof-asm-goalisar-keywords-proof-asm-goal393,6460 (defconst isar-keywords-proof-scriptisar-keywords-proof-script396,6515 isar/isar-mmm.el,129 (defconst isar-start-latex-regexp isar-start-latex-regexp23,697 (defconst isar-start-sml-regexp isar-start-sml-regexp35,1130 isar/isar-syntax.el,4921 (defconst isar-script-syntax-table-entries isar-script-syntax-table-entries18,414 (defconst isar-script-syntax-table-alistisar-script-syntax-table-alist58,1362 (defun isar-init-syntax-table isar-init-syntax-table67,1645 (defun isar-init-output-syntax-table isar-init-output-syntax-table75,1893 (defconst isar-keywords-theory-encloseisar-keywords-theory-enclose90,2308 (defconst isar-keywords-theoryisar-keywords-theory95,2460 (defconst isar-keywords-saveisar-keywords-save100,2605 (defconst isar-keywords-proof-encloseisar-keywords-proof-enclose105,2734 (defconst isar-keywords-proofisar-keywords-proof111,2916 (defconst isar-keywords-proof-contextisar-keywords-proof-context118,3114 (defconst isar-keywords-local-goalisar-keywords-local-goal122,3228 (defconst isar-keywords-improperisar-keywords-improper126,3340 (defconst isar-keywords-outlineisar-keywords-outline131,3479 (defconst isar-keywords-fumeisar-keywords-fume134,3544 (defconst isar-keywords-indent-openisar-keywords-indent-open141,3762 (defconst isar-keywords-indent-closeisar-keywords-indent-close147,3946 (defconst isar-keywords-indent-encloseisar-keywords-indent-enclose151,4051 (defun isar-regexp-simple-alt isar-regexp-simple-alt159,4230 (defun isar-ids-to-regexp isar-ids-to-regexp179,4991 (defconst isar-ext-first isar-ext-first213,6259 (defconst isar-ext-rest isar-ext-rest214,6326 (defconst isar-long-id-stuff isar-long-id-stuff216,6398 (defconst isar-id isar-id217,6472 (defconst isar-idx isar-idx218,6542 (defconst isar-string isar-string220,6601 (defconst isar-any-command-regexpisar-any-command-regexp222,6661 (defconst isar-name-regexpisar-name-regexp226,6795 (defconst isar-tac-regexpisar-tac-regexp232,7090 (defconst isar-save-command-regexpisar-save-command-regexp236,7198 (defconst isar-global-save-command-regexpisar-global-save-command-regexp239,7299 (defconst isar-goal-command-regexpisar-goal-command-regexp242,7413 (defconst isar-local-goal-command-regexpisar-local-goal-command-regexp245,7521 (defconst isar-comment-start isar-comment-start248,7634 (defconst isar-comment-end isar-comment-end249,7669 (defconst isar-comment-start-regexp isar-comment-start-regexp250,7702 (defconst isar-comment-end-regexp isar-comment-end-regexp251,7773 (defconst isar-string-start-regexp isar-string-start-regexp253,7841 (defconst isar-string-end-regexp isar-string-end-regexp254,7889 (defconst isar-antiq-regexpisar-antiq-regexp263,8139 (defface isabelle-class-name-faceisabelle-class-name-face270,8319 (defface isabelle-tfree-name-faceisabelle-tfree-name-face280,8594 (defface isabelle-tvar-name-faceisabelle-tvar-name-face290,8875 (defface isabelle-free-name-faceisabelle-free-name-face300,9155 (defface isabelle-bound-name-faceisabelle-bound-name-face310,9431 (defface isabelle-var-name-faceisabelle-var-name-face320,9710 (defconst isabelle-class-name-face isabelle-class-name-face330,9989 (defconst isabelle-tfree-name-face isabelle-tfree-name-face331,10051 (defconst isabelle-tvar-name-face isabelle-tvar-name-face332,10113 (defconst isabelle-free-name-face isabelle-free-name-face333,10174 (defconst isabelle-bound-name-face isabelle-bound-name-face334,10235 (defconst isabelle-var-name-face isabelle-var-name-face335,10297 (defvar isar-font-lock-keywords-1isar-font-lock-keywords-1337,10358 (defvar isar-output-font-lock-keywords-1isar-output-font-lock-keywords-1351,11287 (defvar isar-goals-font-lock-keywordsisar-goals-font-lock-keywords365,12077 (defconst isar-undo isar-undo396,12711 (defconst isar-kill isar-kill397,12773 (defun isar-remove isar-remove399,12803 (defun isar-undos isar-undos402,12878 (defun isar-cannot-undo isar-cannot-undo406,12984 (defconst isar-undo-fail-regexpisar-undo-fail-regexp410,13055 (defconst isar-undo-skip-regexpisar-undo-skip-regexp414,13193 (defconst isar-undo-ignore-regexpisar-undo-ignore-regexp417,13314 (defconst isar-undo-remove-regexpisar-undo-remove-regexp420,13379 (defconst isar-undo-kill-regexpisar-undo-kill-regexp425,13519 (defconst isar-any-entity-regexpisar-any-entity-regexp431,13661 (defconst isar-named-entity-regexpisar-named-entity-regexp436,13848 (defconst isar-unnamed-entity-regexpisar-unnamed-entity-regexp441,14025 (defconst isar-next-entity-regexpsisar-next-entity-regexps444,14127 (defconst isar-generic-expressionisar-generic-expression452,14434 (defconst isar-indent-any-regexpisar-indent-any-regexp463,14668 (defconst isar-indent-inner-regexpisar-indent-inner-regexp465,14761 (defconst isar-indent-enclose-regexpisar-indent-enclose-regexp467,14827 (defconst isar-indent-open-regexpisar-indent-open-regexp469,14943 (defconst isar-indent-close-regexpisar-indent-close-regexp471,15053 (defconst isar-outline-regexpisar-outline-regexp477,15190 (defconst isar-outline-heading-end-regexp isar-outline-heading-end-regexp481,15343 isar/x-symbol-isar.el,0 lclam/lclam.el,805 (defcustom lclam-prog-name lclam-prog-name15,385 (defcustom lclam-web-pagelclam-web-page21,533 (defun lclam-config lclam-config32,763 (defun lclam-shell-config lclam-shell-config52,1477 (define-derived-mode lclam-proofscript-mode lclam-proofscript-mode72,2136 (define-derived-mode lclam-shell-mode lclam-shell-mode77,2259 (define-derived-mode lclam-response-mode lclam-response-mode82,2393 (define-derived-mode lclam-goals-mode lclam-goals-mode86,2516 (defun lclam-mode lclam-mode94,2744 (defun lclam-pre-shell-start lclam-pre-shell-start107,3027 (define-derived-mode thy-mode thy-mode141,3970 (defvar thy-mode-map thy-mode-map144,4068 (defun thy-add-menus thy-add-menus146,4095 (defun process-thy-file process-thy-file186,6009 (defun update-thy-only update-thy-only192,6210 lego/lego.el,2717 (defcustom lego-tags lego-tags19,493 (defcustom lego-test-all-name lego-test-all-name24,629 (defpgdefault help-menu-entrieshelp-menu-entries30,787 (defpgdefault menu-entriesmenu-entries34,947 (defvar lego-shell-process-outputlego-shell-process-output45,1249 (defconst lego-process-configlego-process-config53,1572 (defconst lego-pretty-set-width lego-pretty-set-width64,2003 (defconst lego-interrupt-regexp lego-interrupt-regexp68,2146 (defcustom lego-www-home-page lego-www-home-page73,2263 (defcustom lego-www-latest-releaselego-www-latest-release78,2387 (defcustom lego-www-refcardlego-www-refcard84,2565 (defcustom lego-library-www-pagelego-library-www-page90,2714 (defvar lego-prog-name lego-prog-name99,2930 (defvar lego-shell-prompt-pattern lego-shell-prompt-pattern102,2999 (defvar lego-shell-cd lego-shell-cd105,3120 (defvar lego-shell-abort-goal-regexp lego-shell-abort-goal-regexp108,3220 (defvar lego-shell-proof-completed-regexp lego-shell-proof-completed-regexp113,3412 (defvar lego-save-command-regexplego-save-command-regexp116,3552 (defvar lego-goal-command-regexplego-goal-command-regexp118,3642 (defvar lego-kill-goal-command lego-kill-goal-command121,3733 (defvar lego-forget-id-command lego-forget-id-command122,3776 (defvar lego-undoable-commands-regexplego-undoable-commands-regexp124,3822 (defvar lego-goal-regexp lego-goal-regexp133,4196 (defvar lego-outline-regexplego-outline-regexp135,4241 (defvar lego-outline-heading-end-regexp lego-outline-heading-end-regexp141,4417 (defvar lego-shell-outline-regexp lego-shell-outline-regexp143,4470 (defvar lego-shell-outline-heading-end-regexp lego-shell-outline-heading-end-regexp144,4522 (define-derived-mode lego-shell-mode lego-shell-mode150,4801 (define-derived-mode lego-mode lego-mode156,4974 (define-derived-mode lego-goals-mode lego-goals-mode167,5271 (defun lego-count-undos lego-count-undos178,5697 (defun lego-goal-command-p lego-goal-command-p198,6516 (defun lego-find-and-forget lego-find-and-forget202,6648 (defun lego-goal-hyp lego-goal-hyp244,8484 (defun lego-state-preserving-p lego-state-preserving-p253,8682 (defvar lego-shell-current-line-width lego-shell-current-line-width269,9385 (defun lego-shell-adjust-line-width lego-shell-adjust-line-width277,9692 (defun lego-pre-shell-start lego-pre-shell-start296,10429 (defun lego-mode-config lego-mode-config303,10626 (defun lego-equal-module-filename lego-equal-module-filename372,12721 (defun lego-shell-compute-new-files-list lego-shell-compute-new-files-list378,12996 (defun lego-shell-mode-config lego-shell-mode-config392,13522 (defun lego-goals-mode-config lego-goals-mode-config438,15365 lego/lego-syntax.el,919 (defconst lego-keywords-goal lego-keywords-goal15,358 (defconst lego-keywords-save lego-keywords-save17,401 (defconst lego-commandslego-commands19,472 (defconst lego-keywordslego-keywords31,1032 (defconst lego-tacticals lego-tacticals36,1209 (defconst lego-error-regexp lego-error-regexp39,1317 (defvar lego-id lego-id42,1476 (defvar lego-ids lego-ids44,1503 (defconst lego-arg-list-regexp lego-arg-list-regexp48,1699 (defun lego-decl-defn-regexp lego-decl-defn-regexp51,1815 (defconst lego-definiendum-alternative-regexplego-definiendum-alternative-regexp59,2187 (defvar lego-font-lock-termslego-font-lock-terms63,2371 (defconst lego-goal-with-hole-regexplego-goal-with-hole-regexp89,3227 (defconst lego-save-with-hole-regexplego-save-with-hole-regexp94,3450 (defvar lego-font-lock-keywords-1lego-font-lock-keywords-199,3667 (defun lego-init-syntax-table lego-init-syntax-table110,4134 lego/x-symbol-lego.el,0 phox/phox.el,898 (defcustom phox-prog-name phox-prog-name31,931 (defcustom phox-web-pagephox-web-page44,1329 (defcustom phox-doc-dir phox-doc-dir50,1479 (defcustom phox-lib-dir phox-lib-dir56,1627 (defcustom phox-tags-program phox-tags-program62,1771 (defcustom phox-tags-doc phox-tags-doc68,1951 (defcustom phox-etags phox-etags74,2089 (defpgdefault menu-entriesmenu-entries95,2541 (defun phox-config phox-config109,2734 (defun phox-shell-config phox-shell-config151,4658 (define-derived-mode phox-mode phox-mode176,5584 (define-derived-mode phox-shell-mode phox-shell-mode190,6002 (define-derived-mode phox-response-mode phox-response-mode195,6130 (define-derived-mode phox-goals-mode phox-goals-mode202,6377 (defun phox-pre-shell-start phox-pre-shell-start224,7278 (defpgdefault completion-tablecompletion-table238,7792 (defpgdefault x-symbol-language x-symbol-language246,7897 phox/phox-extraction.el,603 (defvar phox-prog-orig phox-prog-orig11,480 (defun phox-prog-flags-modify(phox-prog-flags-modify13,548 (defun phox-prog-flags-extract(phox-prog-flags-extract42,1352 (defun phox-prog-flags-erase(phox-prog-flags-erase53,1643 (defun phox-toggle-extraction(phox-toggle-extraction61,1839 (defun phox-compile-theorem(phox-compile-theorem73,2241 (defun phox-compile-theorem-on-cursor(phox-compile-theorem-on-cursor79,2467 (defun phox-output phox-output95,2946 (defun phox-output-theorem phox-output-theorem105,3160 (defun phox-output-theorem-on-cursor(phox-output-theorem-on-cursor112,3460 phox/phox-font.el,64 (defconst phox-font-lock-keywordsphox-font-lock-keywords6,282 phox/phox-fun.el,1049 (defun phox-init-syntax-table phox-init-syntax-table67,2392 (defvar phox-top-keywordsphox-top-keywords83,2865 (defvar phox-proof-keywordsphox-proof-keywords131,3320 (defun phox-find-and-forget phox-find-and-forget172,3670 (defun phox-assert-next-command-interactive phox-assert-next-command-interactive251,6095 (defun phox-depend-theorem(phox-depend-theorem270,6926 (defun phox-eshow-extlist(phox-eshow-extlist279,7216 (defun phox-flag-name(phox-flag-name293,7815 (defun phox-path(phox-path304,8118 (defun phox-print-expression(phox-print-expression315,8355 (defun phox-print-sort-expression(phox-print-sort-expression328,8813 (defun phox-priority-symbols-list(phox-priority-symbols-list339,9126 (defun phox-search-string(phox-search-string351,9499 (defun phox-constraints(phox-constraints366,10027 (defun phox-goals(phox-goals377,10284 (defvar phox-state-menuphox-state-menu389,10494 (defun phox-delete-symbol(phox-delete-symbol414,11484 (defun phox-delete-symbol-on-cursor(phox-delete-symbol-on-cursor420,11693 phox/phox-lang.el,0 phox/phox-outline.el,108 (defun phox-outline-level(phox-outline-level32,1113 (defun phox-setup-outline phox-setup-outline46,1587 phox/phox-pbrpm.el,551 (defun phox-pbrpm-left-paren-p phox-pbrpm-left-paren-p25,1169 (defun phox-pbrpm-right-paren-p phox-pbrpm-right-paren-p32,1372 (defun phox-pbrpm-menu-from-string phox-pbrpm-menu-from-string40,1576 (defun phox-pbrpm-rename-in-cmd phox-pbrpm-rename-in-cmd49,1910 (defun phox-pbrpm-generate-menu phox-pbrpm-generate-menu82,3166 (defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu250,8785 (defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p251,8849 (defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p252,8911 phox/phox-tags.el,483 (defun phox-tags-add-table(phox-tags-add-table21,766 (defun phox-tags-reset-table(phox-tags-reset-table38,1359 (defun phox-tags-add-doc-table(phox-tags-add-doc-table48,1629 (defun phox-tags-add-lib-table(phox-tags-add-lib-table54,1778 (defun phox-tags-add-local-table(phox-tags-add-local-table60,1914 (defun phox-tags-create-local-table(phox-tags-create-local-table66,2097 (defun phox-complete-tag(phox-complete-tag77,2349 (defvar phox-tags-menuphox-tags-menu96,2904 phox/x-symbol-phox.el,2614 (defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts14,449 (defcustom x-symbol-phox-header-groups-alist x-symbol-phox-header-groups-alist29,1056 (defcustom x-symbol-phox-electric-ignore x-symbol-phox-electric-ignore36,1276 (defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts43,1492 (defvar x-symbol-phox-extra-menu-items x-symbol-phox-extra-menu-items46,1593 (defvar x-symbol-phox-token-grammarx-symbol-phox-token-grammar49,1682 (defvar x-symbol-phox-input-token-grammarx-symbol-phox-input-token-grammar63,2473 (defun x-symbol-phox-default-token-list x-symbol-phox-default-token-list69,2728 (defvar x-symbol-phox-user-table x-symbol-phox-user-table81,3046 (defvar x-symbol-phox-generated-data x-symbol-phox-generated-data84,3155 (defvar x-symbol-phox-master-directory x-symbol-phox-master-directory92,3394 (defvar x-symbol-phox-image-searchpath x-symbol-phox-image-searchpath93,3443 (defvar x-symbol-phox-image-cached-dirs x-symbol-phox-image-cached-dirs94,3491 (defvar x-symbol-phox-image-file-truename-alist x-symbol-phox-image-file-truename-alist95,3557 (defvar x-symbol-phox-image-keywords x-symbol-phox-image-keywords96,3610 (defcustom x-symbol-phox-class-alistx-symbol-phox-class-alist103,3831 (defcustom x-symbol-phox-class-face-alist x-symbol-phox-class-face-alist114,4213 (defvar x-symbol-phox-font-lock-keywords x-symbol-phox-font-lock-keywords124,4526 (defvar x-symbol-phox-font-lock-allowed-faces x-symbol-phox-font-lock-allowed-faces126,4573 (defvar x-symbol-phox-case-insensitive x-symbol-phox-case-insensitive132,4798 (defvar x-symbol-phox-token-shape x-symbol-phox-token-shape133,4842 (defvar x-symbol-phox-input-token-ignore x-symbol-phox-input-token-ignore134,4881 (defvar x-symbol-phox-token-list x-symbol-phox-token-list141,5120 (defvar x-symbol-phox-xsymb0-table x-symbol-phox-xsymb0-table143,5165 (defun x-symbol-phox-prepare-table x-symbol-phox-prepare-table164,5624 (defvar x-symbol-phox-tablex-symbol-phox-table172,5800 (defcustom x-symbol-phox-auto-stylex-symbol-phox-auto-style183,6118 (defvar x-symbol-phox-menu-alist x-symbol-phox-menu-alist209,7068 (defvar x-symbol-phox-grid-alist x-symbol-phox-grid-alist211,7158 (defvar x-symbol-phox-decode-atree x-symbol-phox-decode-atree214,7249 (defvar x-symbol-phox-decode-alist x-symbol-phox-decode-alist216,7342 (defvar x-symbol-phox-encode-alist x-symbol-phox-encode-alist218,7439 (defvar x-symbol-phox-nomule-decode-exec x-symbol-phox-nomule-decode-exec222,7596 (defvar x-symbol-phox-nomule-encode-exec x-symbol-phox-nomule-encode-exec224,7696 plastic/plastic.el,4425 (defcustom plastic-tags plastic-tags28,805 (defcustom plastic-test-all-name plastic-test-all-name33,937 (defvar plastic-lit-string plastic-lit-string39,1110 (defcustom plastic-help-menu-listplastic-help-menu-list43,1223 (defvar plastic-shell-process-outputplastic-shell-process-output57,1717 (defconst plastic-process-config plastic-process-config65,2043 (defconst plastic-pretty-set-width plastic-pretty-set-width72,2293 (defconst plastic-interrupt-regexp plastic-interrupt-regexp76,2442 (defcustom plastic-www-home-page plastic-www-home-page82,2563 (defcustom plastic-www-latest-releaseplastic-www-latest-release87,2700 (defcustom plastic-www-refcardplastic-www-refcard93,2873 (defcustom plastic-library-www-pageplastic-library-www-page99,3004 (defcustom plastic-base plastic-base109,3219 (defvar plastic-prog-name plastic-prog-name117,3391 (defun plastic-set-default-env-vars plastic-set-default-env-vars121,3499 (defvar plastic-shell-prompt-pattern plastic-shell-prompt-pattern129,3737 (defvar plastic-shell-cd plastic-shell-cd132,3862 (defvar plastic-shell-abort-goal-regexp plastic-shell-abort-goal-regexp136,4004 (defvar plastic-shell-proof-completed-regexp plastic-shell-proof-completed-regexp140,4172 (defvar plastic-save-command-regexpplastic-save-command-regexp143,4315 (defvar plastic-goal-command-regexpplastic-goal-command-regexp145,4411 (defvar plastic-kill-goal-command plastic-kill-goal-command148,4508 (defvar plastic-forget-id-command plastic-forget-id-command150,4609 (defvar plastic-undoable-commands-regexpplastic-undoable-commands-regexp153,4690 (defvar plastic-goal-regexp plastic-goal-regexp165,5137 (defvar plastic-outline-regexpplastic-outline-regexp167,5185 (defvar plastic-outline-heading-end-regexp plastic-outline-heading-end-regexp173,5364 (defvar plastic-shell-outline-regexp plastic-shell-outline-regexp175,5420 (defvar plastic-shell-outline-heading-end-regexp plastic-shell-outline-heading-end-regexp176,5478 (defvar plastic-error-occurred plastic-error-occurred178,5549 (define-derived-mode plastic-shell-mode plastic-shell-mode187,5881 (define-derived-mode plastic-mode plastic-mode193,6063 (define-derived-mode plastic-goals-mode plastic-goals-mode207,6516 (defun plastic-count-undos plastic-count-undos216,6861 (defun plastic-goal-command-p plastic-goal-command-p236,7737 (defun plastic-find-and-forget plastic-find-and-forget240,7890 (defun plastic-goal-hyp plastic-goal-hyp275,9238 (defun plastic-state-preserving-p plastic-state-preserving-p286,9488 (defvar plastic-shell-current-line-width plastic-shell-current-line-width308,10416 (defun plastic-shell-adjust-line-width plastic-shell-adjust-line-width316,10732 (defun plastic-pre-shell-start plastic-pre-shell-start337,11611 (defun plastic-mode-config plastic-mode-config352,12177 (defun plastic-show-shell-buffer plastic-show-shell-buffer449,15819 (defun plastic-equal-module-filename plastic-equal-module-filename455,15922 (defun plastic-shell-compute-new-files-list plastic-shell-compute-new-files-list461,16200 (defun plastic-shell-mode-config plastic-shell-mode-config477,16737 (defun plastic-goals-mode-config plastic-goals-mode-config528,18927 (defun plastic-small-bar plastic-small-bar540,19209 (defun plastic-large-bar plastic-large-bar542,19298 (defun plastic-preprocessing plastic-preprocessing544,19436 (defun plastic-all-ctxt plastic-all-ctxt595,21264 (defun plastic-send-one-undo plastic-send-one-undo602,21442 (defun plastic-minibuf-cmd plastic-minibuf-cmd612,21770 (defun plastic-minibuf plastic-minibuf624,22249 (defun plastic-synchro plastic-synchro631,22455 (defun plastic-send-minibuf plastic-send-minibuf636,22596 (defun plastic-had-error plastic-had-error644,22925 (defun plastic-reset-error plastic-reset-error648,23100 (defun plastic-call-if-no-error plastic-call-if-no-error651,23239 (defun plastic-show-shell plastic-show-shell656,23443 (define-key plastic-keymap plastic-keymap665,23705 (define-key plastic-keymap plastic-keymap666,23766 (define-key plastic-keymap plastic-keymap667,23827 (define-key plastic-keymap plastic-keymap668,23887 (define-key plastic-keymap plastic-keymap669,23946 (define-key plastic-keymap plastic-keymap670,24005 (defalias 'proof-toolbar-command proof-toolbar-command680,24255 (defalias 'proof-minibuffer-cmd proof-minibuffer-cmd681,24306 plastic/plastic-syntax.el,1015 (defconst plastic-keywords-goal plastic-keywords-goal18,537 (defconst plastic-keywords-save plastic-keywords-save20,583 (defconst plastic-commandsplastic-commands22,657 (defconst plastic-keywordsplastic-keywords35,1267 (defconst plastic-tacticals plastic-tacticals40,1450 (defconst plastic-error-regexp plastic-error-regexp43,1561 (defvar plastic-id plastic-id46,1695 (defvar plastic-ids plastic-ids48,1725 (defconst plastic-arg-list-regexp plastic-arg-list-regexp52,1933 (defun plastic-decl-defn-regexp plastic-decl-defn-regexp55,2052 (defconst plastic-definiendum-alternative-regexpplastic-definiendum-alternative-regexp63,2433 (defvar plastic-font-lock-termsplastic-font-lock-terms67,2626 (defconst plastic-goal-with-hole-regexpplastic-goal-with-hole-regexp89,3339 (defconst plastic-save-with-hole-regexpplastic-save-with-hole-regexp94,3566 (defvar plastic-font-lock-keywords-1plastic-font-lock-keywords-199,3792 (defun plastic-init-syntax-table plastic-init-syntax-table108,4184 twelf/twelf.el,677 (defcustom twelf-root-dirtwelf-root-dir25,591 (defcustom twelf-info-dirtwelf-info-dir31,749 (defun twelf-add-read-declaration twelf-add-read-declaration100,3259 (defun twelf-set-syntax twelf-set-syntax113,3594 (defun twelf-set-word twelf-set-word115,3691 (defun twelf-set-symbol twelf-set-symbol116,3753 (defun twelf-map-string twelf-map-string118,3817 (defun twelf-mode-extra-config twelf-mode-extra-config165,5879 (defconst twelf-syntax-menutwelf-syntax-menu171,6085 (defpacustom chatter chatter185,6452 (defpacustom double-check double-check190,6545 (defpacustom print-implicit print-implicit194,6682 (defpgdefault menu-entriesmenu-entries206,6826 twelf/twelf-font.el,1425 (defun twelf-font-create-face twelf-font-create-face31,836 (defvar twelf-font-dark-background twelf-font-dark-background38,1094 (defvar twelf-font-patternstwelf-font-patterns64,2452 (defun twelf-font-fontify-decl twelf-font-fontify-decl105,4302 (defun twelf-font-fontify-buffer twelf-font-fontify-buffer115,4599 (defun twelf-font-unfontify twelf-font-unfontify122,4858 (defvar font-lock-message-threshold font-lock-message-threshold127,5032 (defun twelf-font-fontify-region twelf-font-fontify-region129,5110 (defun twelf-font-highlight twelf-font-highlight195,7610 (defun twelf-font-find-delimited-comment twelf-font-find-delimited-comment204,8067 (defun twelf-font-find-decl twelf-font-find-decl223,8747 (defun twelf-font-find-binder twelf-font-find-binder239,9237 (defun twelf-font-find-parm twelf-font-find-parm301,11094 (defun twelf-font-find-evar twelf-font-find-evar308,11417 (defun twelf-current-decl twelf-current-decl330,12159 (defun twelf-next-decl twelf-next-decl357,13315 (defconst *whitespace* *whitespace*382,14337 (defconst *twelf-comment-start* *twelf-comment-start*385,14435 (defconst *twelf-id-chars* *twelf-id-chars*388,14564 (defun skip-twelf-comments-and-whitespace skip-twelf-comments-and-whitespace391,14682 (defun twelf-end-of-par twelf-end-of-par403,15156 (defun skip-ahead skip-ahead426,15930 (defun current-line-absolute current-line-absolute438,16352 twelf/twelf-old.el,10513 (defvar twelf-indent twelf-indent212,8771 (defvar twelf-infix-regexp twelf-infix-regexp215,8831 (defvar twelf-server-program twelf-server-program219,9026 (defvar twelf-info-file twelf-info-file222,9107 (defvar twelf-server-display-commands twelf-server-display-commands225,9180 (defvar twelf-highlight-range-function twelf-highlight-range-function230,9428 (defvar twelf-focus-function twelf-focus-function235,9711 (defvar twelf-server-echo-commands twelf-server-echo-commands241,9991 (defvar twelf-save-silently twelf-save-silently244,10112 (defvar twelf-server-timeout twelf-server-timeout248,10284 (defvar twelf-sml-program twelf-sml-program252,10431 (defvar twelf-sml-args twelf-sml-args255,10503 (defvar twelf-sml-display-queries twelf-sml-display-queries258,10569 (defvar twelf-mode-hook twelf-mode-hook261,10677 (defvar twelf-server-mode-hook twelf-server-mode-hook264,10771 (defvar twelf-config-mode-hook twelf-config-mode-hook267,10879 (defvar twelf-sml-mode-hook twelf-sml-mode-hook270,10993 (defvar twelf-to-twelf-sml-mode twelf-to-twelf-sml-mode273,11074 (defvar twelf-config-mode twelf-config-mode276,11166 (defvar *twelf-server-buffer-name* *twelf-server-buffer-name*283,11430 (defvar *twelf-server-buffer* *twelf-server-buffer*286,11534 (defvar *twelf-server-process-name* *twelf-server-process-name*289,11622 (defvar *twelf-config-buffer* *twelf-config-buffer*292,11713 (defvar *twelf-config-time* *twelf-config-time*295,11807 (defvar *twelf-config-list* *twelf-config-list*298,11920 (defvar *twelf-server-last-process-mark* *twelf-server-last-process-mark*301,12032 (defvar *twelf-last-region-sent* *twelf-last-region-sent*304,12150 (defvar *twelf-last-input-buffer* *twelf-last-input-buffer*311,12474 (defvar *twelf-error-pos* *twelf-error-pos*315,12597 (defconst *twelf-read-functions**twelf-read-functions*318,12673 (defconst *twelf-parm-table**twelf-parm-table*325,12911 (defvar twelf-chatter twelf-chatter338,13287 (defvar twelf-double-check twelf-double-check346,13504 (defvar twelf-print-implicit twelf-print-implicit349,13591 (defconst *twelf-track-parms**twelf-track-parms*352,13683 (defun install-basic-twelf-keybindings install-basic-twelf-keybindings363,14107 (defun install-twelf-keybindings install-twelf-keybindings388,15076 (defvar twelf-mode-map twelf-mode-map404,15841 (defvar twelf-mode-syntax-table twelf-mode-syntax-table416,16277 (defun set-twelf-syntax set-twelf-syntax419,16356 (defun set-word set-word421,16453 (defun set-symbol set-symbol422,16508 (defun map-string map-string424,16566 (defconst *whitespace* *whitespace*456,18043 (defconst *twelf-comment-start* *twelf-comment-start*459,18141 (defconst *twelf-id-chars* *twelf-id-chars*462,18270 (defun skip-twelf-comments-and-whitespace skip-twelf-comments-and-whitespace465,18388 (defun twelf-end-of-par twelf-end-of-par477,18862 (defun twelf-current-decl twelf-current-decl500,19636 (defun twelf-mark-decl twelf-mark-decl527,20792 (defun twelf-indent-decl twelf-indent-decl536,21058 (defun twelf-indent-region twelf-indent-region545,21344 (defun twelf-indent-lines twelf-indent-lines556,21668 (defun twelf-comment-indent twelf-comment-indent564,21841 (defun looked-at looked-at575,22197 (defun twelf-indent-line twelf-indent-line580,22369 (defun twelf-indent-line-to twelf-indent-line-to613,24112 (defun twelf-calculate-indent twelf-calculate-indent626,24567 (defun twelf-dsb twelf-dsb641,25191 (defun twelf-mode-variables twelf-mode-variables667,26603 (defun twelf-mode twelf-mode689,27416 (defun twelf-info twelf-info904,35798 (defconst twelf-error-regexptwelf-error-regexp918,36338 (defconst twelf-error-fields-regexptwelf-error-fields-regexp922,36449 (defconst twelf-error-decl-regexptwelf-error-decl-regexp928,36662 (defun looked-at-nth looked-at-nth932,36811 (defun looked-at-nth-int looked-at-nth-int938,36993 (defun twelf-error-parser twelf-error-parser943,37108 (defun twelf-error-decl twelf-error-decl957,37711 (defun twelf-mark-relative twelf-mark-relative963,37890 (defun twelf-mark-absolute twelf-mark-absolute979,38560 (defun twelf-find-decl twelf-find-decl1004,39446 (defun twelf-next-error twelf-next-error1019,40002 (defun twelf-goto-error twelf-goto-error1087,42812 (defun twelf-convert-standard-filename twelf-convert-standard-filename1101,43350 (defun string-member string-member1113,43845 (defun twelf-config-proceed-p twelf-config-proceed-p1125,44337 (defun twelf-save-if-config twelf-save-if-config1132,44599 (defun twelf-config-save-some-buffers twelf-config-save-some-buffers1145,45071 (defun twelf-save-check-config twelf-save-check-config1149,45236 (defun twelf-check-config twelf-check-config1164,45792 (defun twelf-save-check-file twelf-save-check-file1176,46232 (defun twelf-buffer-substring twelf-buffer-substring1192,46955 (defun twelf-buffer-substring-dot twelf-buffer-substring-dot1198,47217 (defun twelf-check-declaration twelf-check-declaration1204,47483 (defun twelf-highlight-range-zmacs twelf-highlight-range-zmacs1227,48543 (defun twelf-focus twelf-focus1233,48793 (defun twelf-focus-noop twelf-focus-noop1239,49059 (defun twelf-type-const twelf-type-const1322,52681 (defvar twelf-server-mode-map twelf-server-mode-map1439,57823 (defconst twelf-server-cd-regexp twelf-server-cd-regexp1451,58375 (defun looked-at-string looked-at-string1454,58515 (defun twelf-server-directory-tracker twelf-server-directory-tracker1458,58656 (defun twelf-input-filter twelf-input-filter1480,59830 (defun twelf-server-mode twelf-server-mode1486,60085 (defun twelf-parse-config twelf-parse-config1519,61302 (defun twelf-server-read-config twelf-server-read-config1537,62194 (defun twelf-server-sync-config twelf-server-sync-config1546,62531 (defun twelf-get-server-buffer twelf-get-server-buffer1576,64037 (defun twelf-init-variables twelf-init-variables1593,64711 (defun twelf-server twelf-server1600,64924 (defun twelf-server-process twelf-server-process1642,66838 (defun twelf-server-display twelf-server-display1651,67244 (defun display-server-buffer display-server-buffer1658,67518 (defun twelf-server-send-command twelf-server-send-command1673,68250 (defun twelf-accept-process-output twelf-accept-process-output1694,69210 (defun twelf-server-wait twelf-server-wait1703,69649 (defun twelf-server-quit twelf-server-quit1745,71787 (defun twelf-server-interrupt twelf-server-interrupt1750,71908 (defun twelf-reset twelf-reset1755,72044 (defun twelf-config-directory twelf-config-directory1760,72188 (defun twelf-server-configure twelf-server-configure1771,72602 (defun natp natp1844,75894 (defun twelf-read-nat twelf-read-nat1848,75995 (defun twelf-read-bool twelf-read-bool1857,76262 (defun twelf-read-limit twelf-read-limit1863,76410 (defun twelf-read-strategy twelf-read-strategy1873,76710 (defun twelf-read-value twelf-read-value1879,76862 (defun twelf-set twelf-set1883,77025 (defun twelf-set-parm twelf-set-parm1896,77502 (defun track-parm track-parm1905,77799 (defun twelf-toggle-double-check twelf-toggle-double-check1910,77973 (defun twelf-toggle-print-implicit twelf-toggle-print-implicit1916,78176 (defun twelf-get twelf-get1922,78389 (defun twelf-timers-reset twelf-timers-reset1936,79015 (defun twelf-timers-show twelf-timers-show1941,79135 (defun twelf-timers-check twelf-timers-check1947,79286 (defun twelf-server-restart twelf-server-restart1953,79451 (defun twelf-config-mode twelf-config-mode1969,80128 (defun twelf-config-mode-check twelf-config-mode-check1985,80727 (defun twelf-tag twelf-tag1994,81177 (defun twelf-tag-files twelf-tag-files2022,82441 (default: *tags-errors*)*tags-errors*2026,82744 (defun twelf-tag-file twelf-tag-file2047,83495 (defun twelf-next-decl twelf-next-decl2082,84717 (defun skip-ahead skip-ahead2107,85739 (defun current-line-absolute current-line-absolute2119,86161 (defun new-temp-buffer new-temp-buffer2124,86371 (defun rev-relativize rev-relativize2135,86755 (defvar twelf-sml-mode-map twelf-sml-mode-map2149,87215 (defconst twelf-sml-prompt-regexp twelf-sml-prompt-regexp2159,87593 (defun expand-dir expand-dir2161,87648 (defun twelf-sml-cd twelf-sml-cd2168,87909 (defconst twelf-sml-cd-regexp twelf-sml-cd-regexp2180,88398 (defun twelf-sml-directory-tracker twelf-sml-directory-tracker2183,88532 (defun twelf-sml-mode twelf-sml-mode2199,89377 (defun twelf-sml twelf-sml2250,91311 (defun switch-to-twelf-sml switch-to-twelf-sml2270,92271 (defun display-twelf-sml-buffer display-twelf-sml-buffer2281,92620 (defun twelf-sml-send-string twelf-sml-send-string2297,93336 (defun twelf-sml-send-region twelf-sml-send-region2302,93540 (defun twelf-sml-send-query twelf-sml-send-query2326,94746 (defun twelf-sml-send-newline twelf-sml-send-newline2336,95143 (defun twelf-sml-send-semicolon twelf-sml-send-semicolon2344,95471 (defun twelf-sml-status twelf-sml-status2352,95805 (defvar twelf-sml-init twelf-sml-init2374,96752 (defun twelf-sml-set-mode twelf-sml-set-mode2377,96929 (defun twelf-sml-quit twelf-sml-quit2403,98106 (defun twelf-sml-process-buffer twelf-sml-process-buffer2408,98218 (defun twelf-sml-process twelf-sml-process2412,98334 (defvar twelf-to-twelf-sml-mode twelf-to-twelf-sml-mode2424,98850 (defun install-twelf-to-twelf-sml-keybindings install-twelf-to-twelf-sml-keybindings2427,98935 (defvar twelf-to-twelf-sml-mode-map twelf-to-twelf-sml-mode-map2437,99320 (defun twelf-to-twelf-sml-mode twelf-to-twelf-sml-mode2448,99833 (defconst twelf-at-point-menutwelf-at-point-menu2498,101700 (defconst twelf-server-state-menutwelf-server-state-menu2508,102072 (defconst twelf-error-menutwelf-error-menu2518,102389 (defconst twelf-tags-menutwelf-tags-menu2524,102533 (defun twelf-toggle-server-display-commands twelf-toggle-server-display-commands2534,102818 (defconst twelf-options-menutwelf-options-menu2537,102942 (defconst twelf-timers-menutwelf-timers-menu2572,104680 (defconst twelf-syntax-menutwelf-syntax-menu2585,105174 (defun twelf-add-menu twelf-add-menu2612,106040 (defun twelf-remove-menu twelf-remove-menu2616,106142 (defun twelf-reset-menu twelf-reset-menu2620,106240 (defun twelf-server-add-menu twelf-server-add-menu2647,107139 (defun twelf-server-remove-menu twelf-server-remove-menu2651,107262 (defun twelf-server-reset-menu twelf-server-reset-menu2655,107374 twelf/x-symbol-twelf.el,0 lib/holes.el,3711 (defvar holes-doc holes-doc35,993 (defvar holes-default-hole holes-default-hole143,4976 (defvar holes-active-hole holes-active-hole147,5145 (defcustom holes-empty-hole-string holes-empty-hole-string154,5354 (defcustom holes-empty-hole-regexp holes-empty-hole-regexp157,5465 (defcustom holes-search-limit holes-search-limit164,5756 (defface active-hole-faceactive-hole-face176,6132 (defface inactive-hole-faceinactive-hole-face188,6580 (defun holes-region-beginning-or-nil holes-region-beginning-or-nil203,7056 (defun holes-region-end-or-nil holes-region-end-or-nil208,7166 (defun holes-copy-active-region holes-copy-active-region213,7264 (defun holes-is-hole-p holes-is-hole-p220,7463 (defun holes-hole-start-position holes-hole-start-position226,7570 (defun holes-hole-end-position holes-hole-end-position233,7759 (defun holes-hole-buffer holes-hole-buffer240,7943 (defun holes-hole-at holes-hole-at247,8118 (defun holes-active-hole-exist-p holes-active-hole-exist-p254,8293 (defun holes-active-hole-start-position holes-active-hole-start-position264,8551 (defun holes-active-hole-end-position holes-active-hole-end-position274,8923 (defun holes-active-hole-buffer holes-active-hole-buffer285,9292 (defun holes-goto-active-hole holes-goto-active-hole296,9598 (defun holes-highlight-hole-as-active holes-highlight-hole-as-active308,9866 (defun holes-highlight-hole holes-highlight-hole318,10178 (defun holes-disable-active-hole holes-disable-active-hole329,10470 (defun holes-set-active-hole holes-set-active-hole347,11013 (defun holes-is-in-hole-p holes-is-in-hole-p360,11359 (defun holes-make-hole holes-make-hole367,11502 (defun holes-make-hole-at holes-make-hole-at393,12248 (defun holes-clear-hole holes-clear-hole413,12724 (defun holes-clear-hole-at holes-clear-hole-at425,13013 (defun holes-map-holes holes-map-holes434,13272 (defun holes-mapcar-holes holes-mapcar-holes442,13455 (defun holes-clear-all-buffer-holes holes-clear-all-buffer-holes448,13622 (defun holes-next holes-next459,13922 (defun holes-next-after-active-hole holes-next-after-active-hole466,14173 (defun holes-set-active-hole-next holes-set-active-hole-next474,14392 (defun holes-replace-segment holes-replace-segment496,14945 (defun holes-replace holes-replace506,15299 (defun holes-replace-active-hole holes-replace-active-hole537,16494 (defun holes-replace-update-active-hole holes-replace-update-active-hole546,16795 (defun holes-delete-update-active-hole holes-delete-update-active-hole567,17485 (defun holes-set-make-active-hole holes-set-make-active-hole574,17699 (defun holes-mouse-replace-active-hole holes-mouse-replace-active-hole609,18825 (defun holes-destroy-hole holes-destroy-hole629,19364 (defun holes-hole-at-event holes-hole-at-event646,19775 (defun holes-mouse-destroy-hole holes-mouse-destroy-hole651,19888 (defun holes-mouse-forget-hole holes-mouse-forget-hole661,20128 (defun holes-mouse-set-make-active-hole holes-mouse-set-make-active-hole677,20438 (defun holes-mouse-set-active-hole holes-mouse-set-active-hole699,20999 (defun holes-set-point-next-hole-destroy holes-set-point-next-hole-destroy711,21263 (defvar hole-maphole-map727,21713 (defvar holes-mode-mapholes-mode-map743,22333 (defun holes-replace-string-by-holes-backward holes-replace-string-by-holes-backward780,23798 (defun holes-skeleton-end-hook holes-skeleton-end-hook798,24499 (defconst holes-jump-doc holes-jump-doc806,24863 (defun holes-abbrev-complete holes-abbrev-complete811,25068 (defun holes-insert-and-expand holes-insert-and-expand829,25764 (defvar holes-mode holes-mode839,26183 (defun holes-mode holes-mode845,26379 lib/holes-load.el,0 lib/proof-compat.el,1194 (defvar proof-running-on-XEmacs proof-running-on-XEmacs24,760 (defvar proof-running-on-Emacs21 proof-running-on-Emacs2126,882 (defvar proof-running-on-win32 proof-running-on-win3230,1129 (defun pg-custom-undeclare-variable pg-custom-undeclare-variable41,1562 (defun subst-char-in-string subst-char-in-string112,3702 (defun replace-regexp-in-string replace-regexp-in-string126,4256 (defconst menuvisiblep menuvisiblep188,6969 (defun set-window-text-height set-window-text-height205,7588 (defmacro save-selected-frame save-selected-frame231,8538 (defun warn warn270,9840 (defun redraw-modeline redraw-modeline277,10095 (defun replace-in-string replace-in-string292,10662 (defun proof-buffer-syntactic-context-emulate proof-buffer-syntactic-context-emulate341,12180 (defvar read-shell-command-mapread-shell-command-map374,13487 (defun read-shell-command read-shell-command392,14189 (defun remassq remassq404,14670 (defun remassoc remassoc416,15059 (defun frames-of-buffer frames-of-buffer429,15504 (defmacro with-selected-window with-selected-window468,16767 (defun pg-pop-to-buffer pg-pop-to-buffer504,17892 (defun process-live-p process-live-p555,19744 lib/span.el,192 (defsubst delete-spans delete-spans24,499 (defsubst span-property-safe span-property-safe28,653 (defsubst set-span-start set-span-start32,792 (defsubst set-span-end set-span-end36,924 lib/span-extent.el,1346 (defsubst make-span make-span16,557 (defsubst detach-span detach-span20,679 (defsubst set-span-endpoints set-span-endpoints24,766 (defsubst set-span-property set-span-property28,899 (defsubst span-read-only span-read-only32,1026 (defsubst span-read-write span-read-write36,1130 (defun span-give-warning span-give-warning40,1237 (defun span-write-warning span-write-warning44,1335 (defsubst span-property span-property49,1535 (defsubst delete-span delete-span53,1650 (defsubst mapcar-spans mapcar-spans59,1821 (defsubst span-at span-at63,2027 (defsubst span-at-before span-at-before67,2144 (defsubst span-start span-start72,2341 (defsubst span-end span-end76,2470 (defsubst prev-span prev-span80,2593 (defsubst next-span next-span84,2739 (defsubst span-live-p span-live-p88,2881 (defun span-raise span-raise96,3153 (defalias 'span-object span-object100,3252 (defalias 'span-string span-string101,3291 (defsubst make-detached-span make-detached-span104,3377 (defsubst span-buffer span-buffer109,3439 (defsubst span-detached-p span-detached-p114,3531 (defsubst set-span-face set-span-face119,3643 (defsubst fold-spans fold-spans124,3739 (defsubst set-span-properties set-span-properties129,3937 (defsubst set-span-keymap set-span-keymap134,4046 (defsubst span-at-event span-at-event139,4161 lib/span-overlay.el,1566 (defalias 'span-start span-start16,543 (defalias 'span-end span-end17,581 (defalias 'set-span-property set-span-property18,615 (defalias 'span-property span-property19,658 (defalias 'make-span make-span20,697 (defalias 'detach-span detach-span21,733 (defalias 'set-span-endpoints set-span-endpoints22,773 (defalias 'span-buffer span-buffer23,818 (defun span-read-only-hook span-read-only-hook25,859 (defun span-read-only span-read-only29,991 (defun span-read-write span-read-write44,1767 (defun span-give-warning span-give-warning50,1986 (defun span-write-warning span-write-warning54,2094 (defun span-lt span-lt61,2420 (defun spans-at-point-prop spans-at-point-prop66,2561 (defun spans-at-region-prop spans-at-region-prop72,2726 (defun span-at span-at80,2970 (defsubst delete-span delete-span86,3184 (defsubst mapcar-spans mapcar-spans93,3406 (defun span-at-before span-at-before97,3610 (defun prev-span prev-span114,4336 (defun next-span next-span120,4487 (defsubst span-live-p span-live-p149,5712 (defun span-raise span-raise155,5878 (defalias 'span-object span-object161,6121 (defun span-string span-string163,6162 (defun set-span-properties set-span-properties169,6344 (defun span-find-span span-find-span181,6599 (defsubst span-at-event span-at-event188,6906 (defun make-detached-span make-detached-span193,7030 (defun fold-spans fold-spans198,7126 (defsubst span-detached-p span-detached-p213,7660 (defsubst set-span-face set-span-face217,7775 (defun set-span-keymap set-span-keymap221,7872 lib/texi-docstring-magic.el,958 (defun texi-docstring-magic-find-face texi-docstring-magic-find-face85,2996 (defun texi-docstring-magic-splice-sep texi-docstring-magic-splice-sep90,3161 (defconst texi-docstring-magic-munge-tabletexi-docstring-magic-munge-table100,3466 (defun texi-docstring-magic-untabify texi-docstring-magic-untabify190,7186 (defun texi-docstring-magic-munge-docstring texi-docstring-magic-munge-docstring200,7501 (defun texi-docstring-magic-texi texi-docstring-magic-texi239,8788 (defun texi-docstring-magic-format-default texi-docstring-magic-format-default252,9228 (defun texi-docstring-magic-texi-for texi-docstring-magic-texi-for268,9863 (defconst texi-docstring-magic-commenttexi-docstring-magic-comment326,11823 (defun texi-docstring-magic texi-docstring-magic332,11977 (defun texi-docstring-magic-face-at-point texi-docstring-magic-face-at-point366,13057 (defun texi-docstring-magic-insert-magic texi-docstring-magic-insert-magic381,13580 lib/xml.el,790 (defsubst xml-node-name xml-node-name82,2907 (defsubst xml-node-attributes xml-node-attributes87,3026 (defsubst xml-node-children xml-node-children92,3144 (defun xml-get-children xml-get-children97,3280 (defun xml-get-attribute xml-get-attribute107,3603 (defun xml-parse-file xml-parse-file123,4067 (defun xml-parse-region xml-parse-region144,4651 (defun xml-parse-tag xml-parse-tag179,5696 (defun xml-parse-attlist xml-parse-attlist284,9165 (defun xml-skip-dtd xml-skip-dtd321,10555 (defun xml-parse-dtd xml-parse-dtd338,11191 (defun xml-parse-elem-type xml-parse-elem-type408,13269 (defun xml-substitute-special xml-substitute-special449,14424 (defun xml-debug-print xml-debug-print470,15231 (defun xml-debug-print-internal xml-debug-print-internal474,15323 mmm/mmm-auto.el,499 (defvar mmm-autoloaded-classesmmm-autoloaded-classes67,2675 (defun mmm-autoload-class mmm-autoload-class85,3320 (defvar mmm-changed-buffers-list mmm-changed-buffers-list125,4887 (defun mmm-major-mode-change mmm-major-mode-change128,4994 (defun mmm-check-changed-buffers mmm-check-changed-buffers141,5515 (defun mmm-mode-on-maybe mmm-mode-on-maybe151,5888 (defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks163,6306 (defun mmm-add-find-file-hook mmm-add-find-file-hook164,6366 mmm/mmm-class.el,626 (defun mmm-get-class-spec mmm-get-class-spec41,1254 (defun mmm-get-class-parameter mmm-get-class-parameter58,1967 (defun mmm-set-class-parameter mmm-set-class-parameter62,2133 (defun* mmm-apply-classmmm-apply-class74,2497 (defun* mmm-apply-classesmmm-apply-classes86,3010 (defun* mmm-apply-all mmm-apply-all106,3776 (defun* mmm-ifymmm-ify118,4203 (defun* mmm-match-regionmmm-match-region184,6890 (defun mmm-match->point mmm-match->point228,8982 (defun mmm-match-and-verify mmm-match-and-verify241,9525 (defun mmm-get-form mmm-get-form267,10583 (defun mmm-default-get-form mmm-default-get-form278,11079 mmm/mmm-cmds.el,1027 (defun mmm-ify-by-class mmm-ify-by-class40,1179 (defun mmm-ify-region mmm-ify-region68,2165 (defun mmm-ify-by-regexpmmm-ify-by-regexp80,2593 (defun mmm-parse-buffer mmm-parse-buffer100,3244 (defun mmm-parse-region mmm-parse-region109,3580 (defun mmm-parse-block mmm-parse-block118,3959 (defun mmm-get-block mmm-get-block135,4710 (defun mmm-clear-current-region mmm-clear-current-region151,5095 (defun mmm-clear-regions mmm-clear-regions156,5259 (defun mmm-clear-all-regions mmm-clear-all-regions161,5405 (defun mmm-reparse-current-region mmm-reparse-current-region169,5569 (defun* mmm-end-current-region mmm-end-current-region188,6185 (defun mmm-insert-region mmm-insert-region226,7768 (defun mmm-insert-by-key mmm-insert-by-key245,8630 (defun mmm-get-insertion-spec mmm-get-insertion-spec291,10888 (defun mmm-insertion-help mmm-insertion-help318,11967 (defun mmm-display-insertion-key mmm-display-insertion-key328,12337 (defun mmm-get-all-insertion-keys mmm-get-all-insertion-keys350,13159 mmm/mmm-compat.el,634 (defvar mmm-xemacs mmm-xemacs40,1291 (defvar mmm-keywords-usedmmm-keywords-used49,1594 (defmacro mmm-regexp-opt mmm-regexp-opt90,2591 (defvar mmm-evaporate-propertymmm-evaporate-property109,3240 (defmacro mmm-set-keymap-default mmm-set-keymap-default127,4006 (defmacro mmm-event-key mmm-event-key136,4448 (defvar skeleton-positions skeleton-positions145,4667 (defun mmm-fixup-skeleton mmm-fixup-skeleton146,4698 (defmacro mmm-make-temp-buffer mmm-make-temp-buffer158,5135 (defvar mmm-font-lock-available-p mmm-font-lock-available-p171,5531 (defmacro mmm-set-font-lock-defaults mmm-set-font-lock-defaults178,5745 mmm/mmm-mason.el,592 (defvar mmm-mason-perl-tagsmmm-mason-perl-tags41,1225 (defvar mmm-mason-pseudo-perl-tagsmmm-mason-pseudo-perl-tags45,1366 (defvar mmm-mason-non-perl-tagsmmm-mason-non-perl-tags48,1442 (defvar mmm-mason-perl-tags-regexpmmm-mason-perl-tags-regexp51,1543 (defvar mmm-mason-pseudo-perl-tags-regexpmmm-mason-pseudo-perl-tags-regexp56,1738 (defvar mmm-mason-tag-names-regexpmmm-mason-tag-names-regexp61,1955 (defun mmm-mason-verify-inline mmm-mason-verify-inline66,2175 (defun mmm-mason-start-line mmm-mason-start-line154,5041 (defun mmm-mason-end-line mmm-mason-end-line159,5106 mmm/mmm-mode.el,1496 (defun mmm-mode mmm-mode106,4116 (defun mmm-mode-on mmm-mode-on312,13247 (defun mmm-mode-off mmm-mode-off352,14969 (defvar mmm-mode-map mmm-mode-map375,15634 (defvar mmm-mode-prefix-map mmm-mode-prefix-map378,15709 (defvar mmm-mode-menu-map mmm-mode-menu-map381,15819 (defun mmm-define-key mmm-define-key384,15910 (define-key mmm-mode-prefix-map mmm-mode-prefix-map406,16585 (define-key mmm-mode-prefix-map mmm-mode-prefix-map413,16843 (define-key mmm-mode-map mmm-mode-map416,16954 (define-key mmm-mode-menu-map mmm-mode-menu-map419,17056 (define-key mmm-mode-menu-map mmm-mode-menu-map421,17128 (define-key mmm-mode-menu-map mmm-mode-menu-map423,17187 (define-key mmm-mode-menu-map mmm-mode-menu-map425,17268 (define-key mmm-mode-menu-map mmm-mode-menu-map427,17349 (define-key mmm-mode-menu-map mmm-mode-menu-map429,17436 (define-key mmm-mode-menu-map mmm-mode-menu-map432,17530 (define-key mmm-mode-menu-map mmm-mode-menu-map434,17590 (define-key mmm-mode-menu-map mmm-mode-menu-map437,17681 (define-key mmm-mode-menu-map mmm-mode-menu-map439,17741 (define-key mmm-mode-menu-map mmm-mode-menu-map441,17848 (define-key mmm-mode-menu-map mmm-mode-menu-map443,17933 (define-key mmm-mode-menu-map mmm-mode-menu-map446,18019 (define-key mmm-mode-menu-map mmm-mode-menu-map448,18079 (define-key mmm-mode-menu-map mmm-mode-menu-map450,18192 (define-key mmm-mode-menu-map mmm-mode-menu-map452,18277 (define-key mmm-mode-map mmm-mode-map455,18360 mmm/mmm-region.el,2300 (defun mmm-overlay-at mmm-overlay-at51,1642 (defun mmm-overlays-at mmm-overlays-at56,1843 (defun mmm-included-p mmm-included-p69,2525 (defun mmm-overlays-in mmm-overlays-in82,2903 (defun mmm-sort-overlays mmm-sort-overlays100,3840 (defvar mmm-current-overlay mmm-current-overlay109,4110 (defvar mmm-previous-overlay mmm-previous-overlay114,4325 (defvar mmm-current-submode mmm-current-submode119,4513 (defvar mmm-previous-submode mmm-previous-submode124,4713 (defun mmm-update-current-submode mmm-update-current-submode129,4886 (defun mmm-set-current-submode mmm-set-current-submode141,5364 (defun mmm-submode-at mmm-submode-at152,5856 (defun mmm-match-front mmm-match-front161,6139 (defun mmm-match-back mmm-match-back177,6780 (defun mmm-front-start mmm-front-start195,7402 (defun mmm-back-end mmm-back-end203,7672 (defun mmm-make-marker mmm-make-marker216,7969 (defun* mmm-make-regionmmm-make-region228,8428 (defun mmm-get-face mmm-get-face286,11150 (defun mmm-clear-overlays mmm-clear-overlays300,11459 (defun mmm-update-mode-info mmm-update-mode-info314,11871 (defun mmm-update-submode-region mmm-update-submode-region397,16038 (defun mmm-add-hooks mmm-add-hooks417,16958 (defun mmm-remove-hooks mmm-remove-hooks421,17093 (defun mmm-get-local-variables-list mmm-get-local-variables-list427,17220 (defun mmm-get-locals mmm-get-locals447,18140 (defun mmm-get-saved-local mmm-get-saved-local460,18721 (defun mmm-set-local-variables mmm-set-local-variables464,18886 (defun mmm-get-saved-local-variables mmm-get-saved-local-variables475,19327 (defun mmm-save-changed-local-variables mmm-save-changed-local-variables483,19644 (defun mmm-clear-local-variables mmm-clear-local-variables502,20502 (defun mmm-enable-font-lock mmm-enable-font-lock513,20781 (defun mmm-update-font-lock-buffer mmm-update-font-lock-buffer521,21041 (defun mmm-refontify-maybe mmm-refontify-maybe534,21564 (defun mmm-submode-changes-in mmm-submode-changes-in545,21921 (defun mmm-regions-in mmm-regions-in558,22406 (defun mmm-regions-alist mmm-regions-alist572,22954 (defun mmm-fontify-region mmm-fontify-region589,23600 (defun mmm-fontify-region-list mmm-fontify-region-list607,24494 (defun mmm-beginning-of-syntax mmm-beginning-of-syntax629,25412 mmm/mmm-rpm.el,242 (defconst mmm-rpm-sh-start-tagsmmm-rpm-sh-start-tags48,1617 (defvar mmm-rpm-sh-end-tagsmmm-rpm-sh-end-tags53,1841 (defvar mmm-rpm-sh-start-regexpmmm-rpm-sh-start-regexp57,2015 (defvar mmm-rpm-sh-end-regexpmmm-rpm-sh-end-regexp61,2193 mmm/mmm-sample.el,269 (defvar mmm-here-doc-mode-alist mmm-here-doc-mode-alist81,2448 (defun mmm-here-doc-get-mode mmm-here-doc-get-mode90,2933 (defun mmm-file-variables-verify mmm-file-variables-verify196,6459 (defun mmm-file-variables-find-back mmm-file-variables-find-back220,7495 mmm/mmm-univ.el,52 (defun mmm-univ-get-mode mmm-univ-get-mode38,1205 mmm/mmm-utils.el,371 (defmacro mmm-valid-buffer mmm-valid-buffer41,1299 (defmacro mmm-save-all mmm-save-all60,1943 (defun mmm-format-string mmm-format-string73,2232 (defun mmm-format-matches mmm-format-matches84,2684 (defmacro mmm-save-keyword mmm-save-keyword105,3362 (defmacro mmm-save-keywords mmm-save-keywords113,3690 (defun mmm-looking-back-at mmm-looking-back-at126,4224 mmm/mmm-vars.el,3586 (defgroup mmm mmm86,2527 (defvar mmm-c-derived-modesmmm-c-derived-modes93,2637 (defvar mmm-save-local-variables mmm-save-local-variables96,2743 (defvar mmm-buffer-saved-locals mmm-buffer-saved-locals176,6248 (defvar mmm-region-saved-locals-defaults mmm-region-saved-locals-defaults181,6448 (defvar mmm-region-saved-locals-for-dominant mmm-region-saved-locals-for-dominant187,6708 (defgroup mmm-faces mmm-faces197,7085 (defcustom mmm-submode-decoration-level mmm-submode-decoration-level203,7256 (defface mmm-init-submode-face mmm-init-submode-face217,7966 (defface mmm-cleanup-submode-face mmm-cleanup-submode-face221,8106 (defface mmm-declaration-submode-face mmm-declaration-submode-face225,8243 (defface mmm-comment-submode-face mmm-comment-submode-face229,8389 (defface mmm-output-submode-face mmm-output-submode-face233,8542 (defface mmm-special-submode-face mmm-special-submode-face237,8691 (defface mmm-code-submode-face mmm-code-submode-face241,8855 (defface mmm-default-submode-face mmm-default-submode-face245,8994 (defcustom mmm-mode-string mmm-mode-string253,9232 (defcustom mmm-submode-mode-line-format mmm-submode-mode-line-format258,9363 (defvar mmm-classes mmm-classes268,9635 (defvar mmm-global-classes mmm-global-classes274,9880 (defcustom mmm-mode-ext-classes-alist mmm-mode-ext-classes-alist281,10062 (defun mmm-add-mode-ext-class mmm-add-mode-ext-class300,10880 (defcustom mmm-major-mode-preferencesmmm-major-mode-preferences309,11205 (defun mmm-add-to-major-mode-preferences mmm-add-to-major-mode-preferences327,12003 (defun mmm-ensure-modename mmm-ensure-modename343,12789 (defun mmm-modename->function mmm-modename->function352,13099 (defcustom mmm-mode-prefix-key mmm-mode-prefix-key366,13557 (defcustom mmm-command-modifiers mmm-command-modifiers371,13684 (defcustom mmm-insert-modifiers mmm-insert-modifiers385,14317 (defcustom mmm-use-old-command-keys mmm-use-old-command-keys400,14995 (defun mmm-use-old-command-keys mmm-use-old-command-keys410,15459 (defcustom mmm-mode-hook mmm-mode-hook418,15658 (defun mmm-run-constructed-hook mmm-run-constructed-hook438,16468 (defun mmm-run-major-hook mmm-run-major-hook446,16854 (defun mmm-run-submode-hook mmm-run-submode-hook449,16931 (defvar mmm-class-hooks-run mmm-class-hooks-run452,17018 (defun mmm-run-class-hook mmm-run-class-hook457,17190 (defcustom mmm-major-mode-hook mmm-major-mode-hook465,17391 (defun mmm-run-major-mode-hook mmm-run-major-mode-hook479,18022 (defcustom mmm-global-mode mmm-global-mode486,18160 (defcustom mmm-never-modesmmm-never-modes503,18748 (defvar mmm-set-file-name-for-modes mmm-set-file-name-for-modes521,19048 (defvar mmm-mode mmm-mode532,19369 (defvar mmm-primary-mode mmm-primary-mode540,19577 (defvar mmm-classes-alist mmm-classes-alist548,19795 (defun mmm-add-classes mmm-add-classes668,26175 (defun mmm-add-group mmm-add-group673,26340 (defconst mmm-version mmm-version686,26804 (defun mmm-version mmm-version689,26869 (defvar mmm-temp-buffer-name mmm-temp-buffer-name696,27012 (defvar mmm-interactive-history mmm-interactive-history702,27142 (defun mmm-add-to-history mmm-add-to-history708,27411 (defun mmm-clear-history mmm-clear-history711,27494 (defvar mmm-mode-ext-classes mmm-mode-ext-classes719,27679 (defun mmm-get-mode-ext-classes mmm-get-mode-ext-classes724,27890 (defun mmm-clear-mode-ext-classes mmm-clear-mode-ext-classes733,28266 (defun mmm-mode-ext-applies mmm-mode-ext-applies737,28391 (defun mmm-get-all-classes mmm-get-all-classes751,28875 TODO.developer,1307 function to to387,15630 $Id: TODO.developer,2,21 This is an outline file. Use C-c C-n,4,77 X 55,1529 *** C Improved configurability of command settings,186,7011 We should let command settings,187,7068 We should let command settings, etc,187,7068 - XEmacs pg forces on font-lock,337,13217 Save foo;413,16753 *** A Doc new bits: font lock keywords,483,19454 *** A Doc new bits: font lock keywords, filename %e,483,19454 Added proof-{script,484,19511 Added proof-{script,shell,484,19511 Added proof-{script,shell,goals,484,19511 Presently used only in proof-easy-config,485,19571 - Mention configuring function menus,496,19907 - document mouse functions,498,19993 - document mouse functions, proof-cd,498,19993 - document mouse functions, proof-cd, process quit timeout,498,19993 X-Symbol,499,20056 X-Symbol, prog-name-guess,499,20056 *** D Fix INFO-DIR-ENTRY in 513,20564 *** C Fixing up errors caused by pbp-generated commands; currently,579,23041 should mean generates an error. With LEGO pbp,582,23247 tactic which always succeeds,583,23311 decodes annotations eagerly. Lazily would be faster,591,23667 the tech report claims --- djs: probably not much faster,592,23736 *** 6. Update Emacs and prover versions in texi,681,26739 doc/ProofGeneral.texi,5799 @node TopTop166,5021 @node PrefacePreface203,6128 @node Latest news for 3.5 and 3.6Latest news for 3.5 and 3.6226,6724 @node FutureFuture265,8412 @node CreditsCredits300,9962 @node Introducing Proof GeneralIntroducing Proof General398,13377 @node Quick start guideQuick start guide453,15369 @node Features of Proof GeneralFeatures of Proof General507,17938 @node Supported proof assistantsSupported proof assistants596,21863 @node Prerequisites for this manualPrerequisites for this manual648,23859 @node Organization of this manualOrganization of this manual692,25485 @node Basic Script ManagementBasic Script Management718,26312 @node Walkthrough example in Isabelle/IsarWalkthrough example in Isabelle/Isar737,26917 @node Proof scriptsProof scripts964,35452 @node Script buffersScript buffers1007,37572 @node Locked queue and editing regionsLocked queue and editing regions1029,38149 @node Goal-save sequencesGoal-save sequences1085,40296 @node Active scripting bufferActive scripting buffer1122,41782 @node Summary of Proof General buffersSummary of Proof General buffers1191,45202 @node Script editing commandsScript editing commands1253,47876 @node Script processing commandsScript processing commands1331,50734 @node Proof assistant commandsProof assistant commands1459,56035 @node Toolbar commandsToolbar commands1605,60922 @node Interrupting during trace outputInterrupting during trace output1629,61851 @node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing1668,63774 @node Goals buffer commandsGoals buffer commands1682,64274 @node Advanced Script ManagementAdvanced Script Management1771,67806 @node Visibility of completed proofsVisibility of completed proofs1802,68960 @node Switching between proof scriptsSwitching between proof scripts1857,70883 @node View of processed files View of processed files 1894,72855 @node Retracting across filesRetracting across files1954,75906 @node Asserting across filesAsserting across files1967,76537 @node Automatic multiple file handlingAutomatic multiple file handling1980,77103 @node Escaping script managementEscaping script management2005,78137 @node Experimental featuresExperimental features2063,80340 @node Support for other PackagesSupport for other Packages2097,81602 @node Syntax highlightingSyntax highlighting2129,82477 @node X-Symbol supportX-Symbol support2168,84098 @node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)2227,86644 @node Support for outline modeSupport for outline mode2286,88774 @node Support for completionSupport for completion2312,89904 @node Support for tagsSupport for tags2369,92069 @node Customizing Proof GeneralCustomizing Proof General2421,94397 @node Basic optionsBasic options2461,96067 @node How to customizeHow to customize2485,96825 @node Display customizationDisplay customization2536,98927 @node User optionsUser options2661,104161 @node Changing facesChanging faces2915,113167 @node Tweaking configuration settingsTweaking configuration settings2990,115836 @node Hints and TipsHints and Tips3047,118361 @node Adding your own keybindingsAdding your own keybindings3066,118962 @node Using file variablesUsing file variables3122,121495 @node Using abbreviationsUsing abbreviations3175,123318 @node LEGO Proof GeneralLEGO Proof General3214,124733 @node LEGO specific commandsLEGO specific commands3255,126102 @node LEGO tagsLEGO tags3275,126557 @node LEGO customizationsLEGO customizations3285,126804 @node Coq Proof GeneralCoq Proof General3317,127722 @node Coq-specific commandsCoq-specific commands3333,128131 @node Coq-specific variablesCoq-specific variables3355,128638 @node Editing multiple proofsEditing multiple proofs3377,129296 @node User-loaded tacticsUser-loaded tactics3401,130404 @node Holes featureHoles feature3465,132878 @node Isabelle Proof GeneralIsabelle Proof General3492,134164 @node Classic IsabelleClassic Isabelle3561,137487 @node ML filesML files3577,137925 @node Theory filesTheory files3648,140350 @node General commands for IsabelleGeneral commands for Isabelle3702,142821 @node Specific commands for IsabelleSpecific commands for Isabelle3714,143303 @node Isabelle customizationsIsabelle customizations3743,144243 @node Isabelle/IsarIsabelle/Isar3808,146341 @node General commands for Isabelle/IsarGeneral commands for Isabelle/Isar3829,147104 @node Specific commands for Isabelle/IsarSpecific commands for Isabelle/Isar3836,147358 @node Logics and SettingsLogics and Settings3923,149886 @node HOL Proof GeneralHOL Proof General3964,151574 @node Shell Proof GeneralShell Proof General4005,153358 @node Obtaining and InstallingObtaining and Installing4041,154816 @node Obtaining Proof GeneralObtaining Proof General4057,155229 @node Installing Proof General from tarballInstalling Proof General from tarball4088,156468 @node Installing Proof General from RPM packageInstalling Proof General from RPM package4113,157300 @node Setting the names of binariesSetting the names of binaries4128,157708 @node Notes for syssiesNotes for syssies4156,158648 @node Known BugsKnown Bugs4229,161581 @node ReferencesReferences4242,161982 @node History of Proof GeneralHistory of Proof General4282,163006 @node Old News for 3.0Old News for 3.04373,167108 @node Old News for 3.1Old News for 3.14443,170802 @node Old News for 3.2Old News for 3.24469,171974 @node Old News for 3.3Old News for 3.34530,174977 @node Old News for 3.4Old News for 3.44549,175874 @node Function IndexFunction Index4572,176930 @node Variable IndexVariable Index4576,177006 @node Keystroke IndexKeystroke Index4580,177086 @node Concept IndexConcept Index4584,177152 doc/PG-adapting.texi,3863 @node TopTop157,4773 @node IntroductionIntroduction195,5918 @node FutureFuture236,7571 @node CreditsCredits272,9167 @node Beginning with a New ProverBeginning with a New Prover282,9459 @node Overview of adding a new proverOverview of adding a new prover323,11408 @node Demonstration instance and easy configurationDemonstration instance and easy configuration397,14829 @node Major modes used by Proof GeneralMajor modes used by Proof General466,18220 @node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands539,21303 @node Settings for generic user-level commandsSettings for generic user-level commands554,21849 @node Menu configurationMenu configuration599,23585 @node Toolbar configurationToolbar configuration623,24503 @node Proof Script SettingsProof Script Settings681,26748 @node Recognizing commands and commentsRecognizing commands and comments703,27328 @node Recognizing proofsRecognizing proofs824,32855 @node Recognizing other elementsRecognizing other elements936,37669 @node Configuring undo behaviourConfiguring undo behaviour1062,43147 @node Nested proofsNested proofs1200,48488 @node Safe (state-preserving) commandsSafe (state-preserving) commands1240,50115 @node Activate scripting hookActivate scripting hook1263,51061 @node Automatic multiple filesAutomatic multiple files1287,51925 @node CompletionsCompletions1309,52772 @node Proof Shell SettingsProof Shell Settings1349,54250 @node Proof shell commandsProof shell commands1380,55532 @node Script input to the shellScript input to the shell1543,62407 @node Settings for matching various output from proof processSettings for matching various output from proof process1610,65450 @node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1741,71214 @node Hooks and other settingsHooks and other settings1951,80767 @node Goals Buffer SettingsGoals Buffer Settings2047,84600 @node Splash Screen SettingsSplash Screen Settings2124,87708 @node Global ConstantsGlobal Constants2150,88466 @node Handling Multiple FilesHandling Multiple Files2176,89315 @node Configuring Editing SyntaxConfiguring Editing Syntax2328,97099 @node Configuring Font LockConfiguring Font Lock2385,99216 @node Configuring X-SymbolConfiguring X-Symbol2472,103459 @node Writing More Lisp CodeWriting More Lisp Code2532,105982 @node Default values for generic settingsDefault values for generic settings2549,106627 @node Adding prover-specific configurationsAdding prover-specific configurations2579,107710 @node Useful variablesUseful variables2622,108980 @node Useful functions and macrosUseful functions and macros2648,109774 @node Internals of Proof GeneralInternals of Proof General2750,113651 @node SpansSpans2778,114559 @node Proof General site configurationProof General site configuration2791,114933 @node Configuration variable mechanismsConfiguration variable mechanisms2871,118077 @node Global variablesGlobal variables2989,123313 @node Proof script modeProof script mode3059,125863 @node Proof shell modeProof shell mode3318,137518 @node DebuggingDebugging3724,153565 @node Plans and IdeasPlans and Ideas3767,154460 @node Proof by pointing and similar featuresProof by pointing and similar features3788,155182 @node Granularity of atomic command sequencesGranularity of atomic command sequences3826,156840 @node Browser mode for script files and theoriesBrowser mode for script files and theories3871,159065 @node Demonstration InstantiationsDemonstration Instantiations3901,160096 @node demoisa-easy.eldemoisa-easy.el3917,160527 @node demoisa.eldemoisa.el3980,162765 @node Function IndexFunction Index4148,168281 @node Variable IndexVariable Index4152,168357 @node Concept IndexConcept Index4161,168536