acl2/acl2.el,0 acl2/x-symbol-acl2.el,0 coq/coq-abbrev.el,109 (defpgdefault menu-entriesmenu-entries147,7898 (defpgdefault help-menu-entrieshelp-menu-entries341,18188 coq/coq-abbrev-V7.el,49 (defpgdefault menu-entriesmenu-entries119,5878 coq/coq.el,5468 (defcustom coq-prog-name coq-prog-name13,355 (defcustom coq-compile-file-command coq-compile-file-command18,464 (defcustom coq-default-undo-limit coq-default-undo-limit28,833 (defconst coq-shell-init-cmd coq-shell-init-cmd33,961 (defconst coq-shell-restart-cmd coq-shell-restart-cmd46,1384 (defvar coq-shell-prompt-pattern coq-shell-prompt-pattern53,1642 (defvar coq-shell-cd coq-shell-cd58,1850 (defvar coq-shell-abort-goal-regexp coq-shell-abort-goal-regexp64,2051 (defvar coq-shell-proof-completed-regexp coq-shell-proof-completed-regexp67,2177 (defvar coq-goal-regexpcoq-goal-regexp70,2308 (defun coq-library-directory coq-library-directory79,2497 (defcustom coq-tags coq-tags86,2677 (defconst coq-interrupt-regexp coq-interrupt-regexp91,2826 (defcustom coq-www-home-page coq-www-home-page96,2946 (defun coq-insert-section coq-insert-section112,3196 (defconst module-kinds-table module-kinds-table121,3453 (defconst modtype-kinds-tablemodtype-kinds-table125,3589 (defun coq-insert-module coq-insert-module129,3718 (defvar coq-outline-regexpcoq-outline-regexp150,4475 (defvar coq-outline-heading-end-regexp coq-outline-heading-end-regexp155,4884 (defvar coq-shell-outline-regexp coq-shell-outline-regexp157,4943 (defvar coq-shell-outline-heading-end-regexp coq-shell-outline-heading-end-regexp158,4993 (defconst coq-kill-goal-command coq-kill-goal-command160,5056 (defconst coq-forget-id-command coq-forget-id-command161,5099 (defconst coq-back-n-command coq-back-n-command162,5145 (defconst coq-state-changing-tactics-regexp coq-state-changing-tactics-regexp166,5207 (defconst coq-state-preserving-tactics-regexp coq-state-preserving-tactics-regexp168,5304 (defconst coq-tactics-regexpcoq-tactics-regexp170,5405 (defconst coq-state-changing-commands-regexpcoq-state-changing-commands-regexp172,5471 (defconst coq-state-preserving-commands-regexp coq-state-preserving-commands-regexp174,5578 (defvar coq-retractable-instruct-regexp coq-retractable-instruct-regexp176,5690 (defvar coq-non-retractable-instruct-regexpcoq-non-retractable-instruct-regexp178,5781 (defvar coq-keywords-sectioncoq-keywords-section181,5880 (defvar coq-section-regexp coq-section-regexp186,6025 (defun coq-set-undo-limit coq-set-undo-limit219,7092 (defconst coq-keywords-decl-defn-regexpcoq-keywords-decl-defn-regexp230,7435 (defun coq-proof-mode-p coq-proof-mode-p238,7823 (defun coq-is-comment-or-proverprocp coq-is-comment-or-proverprocp253,8329 (defun coq-is-goalsave-p coq-is-goalsave-p255,8433 (defun coq-is-module-equal-p coq-is-module-equal-p256,8508 (defun coq-is-def-p coq-is-def-p259,8704 (defun coq-is-decl-defn-p coq-is-decl-defn-p261,8812 (defun coq-state-preserving-command-p coq-state-preserving-command-p266,8979 (defun coq-state-preserving-tactic-p coq-state-preserving-tactic-p269,9113 (defun coq-state-changing-command-p coq-state-changing-command-p272,9245 (defun coq-section-or-module-start-p coq-section-or-module-start-p278,9553 (defun coq-find-and-forget coq-find-and-forget286,9806 (defvar coq-current-goal coq-current-goal378,14373 (defun coq-goal-hyp coq-goal-hyp381,14438 (defun coq-state-preserving-p coq-state-preserving-p394,14868 (defun coq-SearchIsos coq-SearchIsos401,15185 (defun coq-guess-or-ask-for-string coq-guess-or-ask-for-string415,15619 (defun coq-Print coq-Print425,15913 (defun coq-Check coq-Check434,16171 (defun coq-Show coq-Show443,16413 (defun coq-PrintHint coq-PrintHint464,17099 (defun coq-end-Section coq-end-Section470,17242 (defun coq-Compile coq-Compile488,17826 (defun coq-intros coq-intros495,18006 (define-key coq-keymap coq-keymap512,18683 (define-key coq-keymap coq-keymap513,18734 (define-key coq-keymap coq-keymap514,18793 (define-key coq-keymap coq-keymap515,18851 (define-key coq-keymap coq-keymap516,18907 (define-key coq-keymap coq-keymap517,18962 (define-key coq-keymap coq-keymap518,19012 (define-key coq-keymap coq-keymap519,19062 (define-key global-map global-map528,19571 (defun coq-guess-command-line coq-guess-command-line587,21565 (defun coq-pre-shell-start coq-pre-shell-start609,22371 (defun coq-mode-config coq-mode-config620,22892 (defun coq-shell-mode-config coq-shell-mode-config726,26637 (defun coq-goals-mode-config coq-goals-mode-config765,28272 (defun coq-response-config coq-response-config772,28503 (defun coq-maybe-compile-buffer coq-maybe-compile-buffer792,29219 (defun coq-ancestors-of coq-ancestors-of829,30753 (defun coq-all-ancestors-of coq-all-ancestors-of852,31720 (defconst coq-require-command-regexp coq-require-command-regexp864,32113 (defun coq-process-require-command coq-process-require-command869,32322 (defun coq-included-children coq-included-children874,32449 (defun coq-process-file coq-process-file895,33288 (defpacustom print-only-first-subgoal print-only-first-subgoal909,33786 (defpacustom print-fully-explicit print-fully-explicit914,33937 (defpacustom print-coercions print-coercions919,34084 (defpacustom print-match-wildcards print-match-wildcards924,34227 (defpacustom time-commands time-commands930,34409 (defpacustom auto-compile-vos auto-compile-vos934,34520 (defpacustom translate-to-v8 translate-to-v8956,35475 (defun coq-preprocessing coq-preprocessing965,35691 (defun coq-fake-constant-markup coq-fake-constant-markup980,36110 (defun coq-create-span-menu coq-create-span-menu1002,36917 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,2691 (defun coq-find-end coq-find-end107,3085 (defun coq-current-command-string coq-current-command-string117,3356 (defun is-at-a-space-or-tab is-at-a-space-or-tab125,3555 (defun only-spaces-on-line only-spaces-on-line131,3759 (defun find-reg find-reg138,4007 (defun coq-back-to-indentation-prevline coq-back-to-indentation-prevline152,4382 (defun coq-find-unclosed coq-find-unclosed181,5618 (defun coq-find-at-same-level-zero coq-find-at-same-level-zero208,6799 (defun coq-find-unopened coq-find-unopened236,7883 (defun coq-find-last-unopened coq-find-last-unopened282,9236 (defun coq-end-offset coq-end-offset295,9640 (defun coq-indent-command-offset coq-indent-command-offset323,10459 (defun coq-indent-expr-offset coq-indent-expr-offset368,12219 (defun coq-indent-offset coq-indent-offset480,16422 (defun coq-indent-calculate coq-indent-calculate500,17085 (defun proof-indent-line proof-indent-line514,17532 coq/coq-syntax.el,3214 (defvar coq-version-is-V74 coq-version-is-V7416,415 (defvar coq-version-is-V7 coq-version-is-V717,447 (defvar coq-version-is-V6 coq-version-is-V625,767 (defvar coq-version-is-V7 coq-version-is-V732,1119 (defvar coq-version-is-V74 coq-version-is-V7440,1529 (defvar coq-version-is-V8 coq-version-is-V849,1988 (defvar coq-keywords-declcoq-keywords-decl124,4579 (defvar coq-keywords-defncoq-keywords-defn139,4935 (defun coq-count-match coq-count-match213,7291 (defun coq-goal-command-p coq-goal-command-p225,7711 (defvar coq-keywords-save-strictcoq-keywords-save-strict245,8295 (defvar coq-keywords-savecoq-keywords-save253,8392 (defun coq-save-command-p coq-save-command-p257,8468 (defvar coq-keywords-kill-goal coq-keywords-kill-goal265,8747 (defcustom coq-user-state-changing-commands coq-user-state-changing-commands271,8797 (defcustom coq-user-state-preserving-commands coq-user-state-preserving-commands283,9194 (defvar coq-keywords-state-preserving-commandscoq-keywords-state-preserving-commands296,9634 (defvar coq-keywords-state-changing-misc-commandscoq-keywords-state-changing-misc-commands343,10745 (defvar coq-keywords-state-changing-commandscoq-keywords-state-changing-commands417,12763 (defvar coq-keywords-commandscoq-keywords-commands427,12960 (defcustom coq-user-state-changing-tactics coq-user-state-changing-tactics433,13110 (defvar coq-state-changing-tacticscoq-state-changing-tactics444,13536 (defcustom coq-user-state-preserving-tactics coq-user-state-preserving-tactics645,16861 (defvar coq-state-preserving-tacticscoq-state-preserving-tactics656,17275 (defvar coq-tacticscoq-tactics660,17373 (defvar coq-retractable-instructcoq-retractable-instruct663,17462 (defvar coq-non-retractable-instructcoq-non-retractable-instruct666,17572 (defvar coq-keywordscoq-keywords670,17694 (defvar coq-tacticalscoq-tacticals675,17859 (defvar coq-reserved-commoncoq-reserved-common697,18242 (defvar coq-reserved-V8coq-reserved-V8713,18435 (defvar coq-reserved-V7coq-reserved-V7724,18539 (defvar coq-reserved coq-reserved729,18614 (defvar coq-symbolscoq-symbols737,18770 (defvar coq-error-regexp coq-error-regexp755,18974 (defvar coq-id coq-id758,19190 (defvar coq-ids coq-ids760,19216 (defun coq-first-abstr-regexp coq-first-abstr-regexp762,19253 (defun coq-next-abstr-regexp coq-next-abstr-regexp765,19341 (defvar coq-font-lock-termscoq-font-lock-terms768,19419 (defconst coq-save-command-regexp-strictcoq-save-command-regexp-strict783,20072 (defconst coq-save-command-regexpcoq-save-command-regexp785,20185 (defconst coq-save-with-hole-regexpcoq-save-with-hole-regexp787,20284 (defconst coq-goal-command-regexpcoq-goal-command-regexp790,20422 (defconst coq-goal-with-hole-regexpcoq-goal-with-hole-regexp792,20521 (defconst coq-decl-with-hole-regexpcoq-decl-with-hole-regexp798,20810 (defconst coq-defn-with-hole-regexpcoq-defn-with-hole-regexp801,20943 (defvar coq-font-lock-keywords-1coq-font-lock-keywords-1804,21083 (defvar coq-font-lock-keywords coq-font-lock-keywords825,22126 (defun coq-init-syntax-table coq-init-syntax-table827,22184 (defconst coq-generic-expressioncoq-generic-expression856,23082 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/holes.el,3536 (defun holes-short-doc holes-short-doc24,736 (defcustom empty-hole-string empty-hole-string149,5370 (defcustom empty-hole-regexp empty-hole-regexp152,5475 (defcustom hole-search-limit hole-search-limit155,6075 (defface active-hole-faceactive-hole-face168,6441 (defface inactive-hole-faceinactive-hole-face178,6898 (defun region-beginning-or-nil region-beginning-or-nil197,7434 (defun region-end-or-nil region-end-or-nil201,7523 (defun copy-active-region copy-active-region205,7602 (defun is-hole-p is-hole-p211,7780 (defun hole-start-position hole-start-position216,7840 (defun hole-end-position hole-end-position221,7977 (defun hole-buffer hole-buffer226,8107 (defun hole-at hole-at231,8229 (defun active-hole-exist-p active-hole-exist-p240,8417 (defun active-hole-start-position active-hole-start-position250,8668 (defun active-hole-end-position active-hole-end-position261,9018 (defun active-hole-buffer active-hole-buffer273,9364 (defun goto-active-hole goto-active-hole284,9644 (defun highlight-hole-as-active highlight-hole-as-active296,9917 (defun highlight-hole highlight-hole306,10224 (defun disable-active-hole disable-active-hole317,10519 (defun set-active-hole set-active-hole335,11028 (defun is-in-hole-p is-in-hole-p347,11329 (defun make-hole make-hole357,11474 (defun make-hole-at make-hole-at382,12289 (defun clear-hole clear-hole401,12731 (defun clear-hole-at clear-hole-at411,12948 (defun map-holes map-holes420,13177 (defun mapcar-holes mapcar-holes426,13291 (defun clear-all-buffer-holes clear-all-buffer-holes430,13390 (defun next-hole next-hole442,13624 (defun next-after-active-hole next-after-active-hole451,13888 (defun set-active-hole-next set-active-hole-next458,14068 (defun set-active-hole-next-after-active set-active-hole-next-after-active475,14425 (defun replace-segment replace-segment486,14583 (defun replace-hole replace-hole502,14899 (defun replace-active-hole replace-active-hole536,16055 (defun replace-update-active-hole replace-update-active-hole545,16338 (defun delete-update-active-hole delete-update-active-hole568,16964 (defun set-make-active-hole set-make-active-hole577,17161 (defun mouse-replace-active-hole mouse-replace-active-hole624,18508 (defun destroy-hole destroy-hole642,18984 (defun hole-at-event hole-at-event657,19295 (defun mouse-destroy-hole mouse-destroy-hole659,19354 (defun mouse-forget-hole mouse-forget-hole667,19528 (defun mouse-set-make-active-hole mouse-set-make-active-hole681,19769 (defun mouse-set-active-hole mouse-set-active-hole701,20220 (defun set-point-next-hole-destroy set-point-next-hole-destroy711,20414 (defun count-char-in-string count-char-in-string775,22661 (defun count-re-in-string count-re-in-string785,22866 (defun count-chars-in-last-expand count-chars-in-last-expand795,23077 (defun count-newlines-in-last-expand count-newlines-in-last-expand799,23166 (defun indent-last-expand indent-last-expand803,23277 (defun count-holes-in-last-expand count-holes-in-last-expand818,23603 (defun replace-string-by-holes replace-string-by-holes822,23722 (defun replace-string-by-holes-backward replace-string-by-holes-backward841,24148 (defun replace-string-by-holes-move-point replace-string-by-holes-move-point872,24966 (defun replace-string-by-holes-backward-move-point replace-string-by-holes-backward-move-point879,25120 (defun holes-abbrev-complete holes-abbrev-complete889,25296 (defun insert-and-expand insert-and-expand911,26098 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-goals.el,1074 (define-derived-mode proof-goals-mode proof-goals-mode28,650 (define-key proof-goals-mode-map proof-goals-mode-map48,1340 (define-key proof-goals-mode-map proof-goals-mode-map51,1423 (define-key proof-goals-mode-map proof-goals-mode-map52,1493 (define-key proof-goals-mode-map proof-goals-mode-map57,1909 (define-key proof-goals-mode-map proof-goals-mode-map59,1982 (define-key proof-goals-mode-map proof-goals-mode-map60,2050 (define-key proof-goals-mode-map proof-goals-mode-map63,2310 (defun proof-goals-config-done proof-goals-config-done78,2574 (defun pg-goals-display pg-goals-display88,2862 (defun pg-goals-analyse-structure pg-goals-analyse-structure137,4805 (defun pg-goals-make-top-span pg-goals-make-top-span261,9651 (defun pg-goals-yank-subterm pg-goals-yank-subterm291,10658 (defun pg-goals-button-action pg-goals-button-action318,11558 (defun proof-expand-path proof-expand-path339,12531 (defun pg-goals-construct-command pg-goals-construct-command348,12775 (defun pg-goals-get-subterm-help pg-goals-get-subterm-help372,13627 generic/pg-init.el,0 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-nxml.el,66 (defun pg-nxml-support-available pg-nxml-support-available9,236 generic/pg-pgip.el,1154 (defalias 'pg-pgip-error pg-pgip-error17,544 (defun pg-pgip-process-packet pg-pgip-process-packet20,593 (defun pg-pgip-process-cmds pg-pgip-process-cmds28,981 (defun pg-pgip-post-process pg-pgip-post-process88,2599 (defun pg-pgip-haspref pg-pgip-haspref125,3616 (defun pg-pgip-default-for pg-pgip-default-for188,5899 (defun pg-pgip-subst-for pg-pgip-subst-for199,6211 (defun pg-pgip-get-type pg-pgip-get-type206,6372 (defun pg-pgip-pgiptype pg-pgip-pgiptype213,6594 (defun pg-pgip-interpret-bool pg-pgip-interpret-bool237,7458 (defun pg-pgip-interpret-int pg-pgip-interpret-int246,7734 (defun pg-pgip-interpret-string pg-pgip-interpret-string251,7897 (defun pg-pgip-interpret-choice pg-pgip-interpret-choice254,7947 (defun pg-pgip-interpret-value pg-pgip-interpret-value274,8642 (defun pg-pgip-get-attr pg-pgip-get-attr297,9267 (defun pg-pgip-get-version pg-pgip-get-version304,9480 (defun pg-prover-interpret-pgip-command pg-prover-interpret-pgip-command312,9712 (defun pg-issue-pgip pg-issue-pgip329,10134 (defun pg-pgip-askprefs pg-pgip-askprefs337,10406 (defun pg-pgip-parsescript pg-pgip-parsescript346,10618 generic/pg-response.el,1673 (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-enable103,3730 (defun proof-three-window-enable proof-three-window-enable125,4450 (defun proof-select-three-b proof-select-three-b129,4514 (defun proof-display-three-b proof-display-three-b144,4983 (defvar pg-frame-configuration pg-frame-configuration158,5477 (defun pg-cache-frame-configuration pg-cache-frame-configuration162,5624 (defun proof-layout-windows proof-layout-windows166,5795 (defun proof-delete-other-frames proof-delete-other-frames207,7608 (defvar pg-response-erase-flag pg-response-erase-flag238,8703 (defun proof-shell-maybe-erase-responseproof-shell-maybe-erase-response241,8818 (defun pg-response-display pg-response-display271,9968 (defun pg-response-display-with-face pg-response-display-with-face288,10790 (defun pg-response-clear-displays pg-response-clear-displays323,12147 (defvar pg-response-next-error pg-response-next-error340,12677 (defun proof-next-error proof-next-error344,12799 (defvar proof-trace-last-fontify-pos proof-trace-last-fontify-pos439,16212 (defun proof-trace-buffer-display proof-trace-buffer-display442,16304 (defun pg-thms-buffer-clear pg-thms-buffer-clear482,17517 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,3521 (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-command413,13595 (defmacro proof-define-assistant-command-witharg proof-define-assistant-command-witharg425,14046 (defun proof-issue-new-command proof-issue-new-command445,14852 (defun proof-cd-sync proof-cd-sync490,16351 (deflocal proof-electric-terminator proof-electric-terminator541,17820 (defun proof-electric-terminator-enable proof-electric-terminator-enable551,18167 (defun proof-electric-term-incomment-fn proof-electric-term-incomment-fn562,18654 (defun proof-process-electric-terminator proof-process-electric-terminator582,19410 (defun proof-electric-terminator proof-electric-terminator609,20561 (defun proof-add-completions proof-add-completions631,21199 (defun proof-script-complete proof-script-complete651,21956 (defun pg-insert-last-output-as-comment pg-insert-last-output-as-comment679,22547 (defun pg-copy-span-contents pg-copy-span-contents710,23775 (defun pg-numth-span-higher-or-lower pg-numth-span-higher-or-lower727,24335 (defun pg-control-span-of pg-control-span-of753,25086 (defun pg-move-span-contents pg-move-span-contents759,25290 (defun pg-fixup-children-span pg-fixup-children-span813,27514 (defun pg-move-region-down pg-move-region-down820,27722 (defun pg-move-region-up pg-move-region-up829,28016 (defun proof-forward-command proof-forward-command859,28856 (defun proof-backward-command proof-backward-command880,29578 (defvar pg-span-context-menu-keymappg-span-context-menu-keymap896,29822 (defun pg-span-for-event pg-span-for-event912,30249 (defun pg-span-context-menu pg-span-context-menu923,30633 (defun pg-toggle-visibility pg-toggle-visibility938,31093 (defun pg-create-in-span-context-menu pg-create-in-span-context-menu948,31415 (defun pg-goals-buffers-hint pg-goals-buffers-hint1020,33968 (defun pg-response-buffers-hint pg-response-buffers-hint1023,34135 (defun pg-jump-to-end-hint pg-jump-to-end-hint1032,34484 (defun pg-processing-complete-hint pg-processing-complete-hint1035,34600 (defun pg-hint pg-hint1051,35286 (defun pg-identifier-under-mouse-query pg-identifier-under-mouse-query1070,35962 (defun proof-imenu-enable proof-imenu-enable1115,37589 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,1487 (defconst pg-xml-name pg-xml-name32,848 (defconst pg-xml-space pg-xml-space33,901 (defconst pg-xml-ref pg-xml-ref34,936 (defconst pg-xml-start-open-elt-regexp pg-xml-start-open-elt-regexp36,1012 (defconst pg-xml-end-open-elt-regexp pg-xml-end-open-elt-regexp38,1106 (defconst pg-xml-close-elt-regexp pg-xml-close-elt-regexp40,1185 (defconst pg-xml-attribute-regexp pg-xml-attribute-regexp42,1276 (defconst pg-xml-attribute-val-regexp pg-xml-attribute-val-regexp44,1364 (defconst pg-xml-comment-start-regexp pg-xml-comment-start-regexp47,1515 (defconst pg-xml-comment-end-regexp pg-xml-comment-end-regexp48,1561 (defconst pg-xml-anymarkup-regexp pg-xml-anymarkup-regexp49,1604 (defconst pg-xml-special-eltspg-xml-special-elts50,1643 (defvar xmlparse xmlparse54,1742 (defun pg-xml-add-text pg-xml-add-text57,1797 (defun pg-xml-parse-buffer pg-xml-parse-buffer64,2009 (defun pg-xml-parse-string pg-xml-parse-string171,5979 (defconst pg-xml-header pg-xml-header188,6468 (defvar pg-xml-doc pg-xml-doc191,6544 (defvar pg-xml-openelts pg-xml-openelts194,6634 (defvar pg-xml-indentp pg-xml-indentp197,6690 (defun pg-xml-encode-entities pg-xml-encode-entities200,6763 (defun pg-xml-begin-write pg-xml-begin-write210,7252 (defun pg-xml-indent pg-xml-indent215,7444 (defun pg-xml-openelt pg-xml-openelt221,7583 (defun pg-xml-closeelt pg-xml-closeelt240,8129 (defun pg-xml-writetext pg-xml-writetext252,8399 (defun pg-xml-doc pg-xml-doc255,8500 generic/_pkg.el,0 generic/proof-autoloads.el,0 generic/proof-compat.el,999 (defun pg-custom-undeclare-variable pg-custom-undeclare-variable28,1002 (defun subst-char-in-string subst-char-in-string99,3142 (defun replace-regexp-in-string replace-regexp-in-string112,3633 (defconst menuvisiblep menuvisiblep174,6346 (defun set-window-text-height set-window-text-height191,6965 (defmacro save-selected-frame save-selected-frame217,7915 (defun warn warn256,9217 (defun redraw-modeline redraw-modeline263,9472 (defun replace-in-string replace-in-string278,10039 (defun proof-buffer-syntactic-context-emulate proof-buffer-syntactic-context-emulate327,11557 (defvar read-shell-command-mapread-shell-command-map360,12864 (defun read-shell-command read-shell-command378,13566 (defun remassq remassq390,14047 (defun remassoc remassoc402,14436 (defun frames-of-buffer frames-of-buffer415,14881 (defmacro with-selected-window with-selected-window454,16144 (defun pg-pop-to-buffer pg-pop-to-buffer490,17269 (defun process-live-p process-live-p541,19121 generic/proof-config.el,16702 (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,17219 (defface proof-declaration-name-faceproof-declaration-name-face469,17477 (defconst proof-declaration-name-face proof-declaration-name-face481,17870 (defface proof-tacticals-name-faceproof-tacticals-name-face486,18106 (defconst proof-tacticals-name-face proof-tacticals-name-face495,18368 (defface proof-tactics-name-faceproof-tactics-name-face500,18598 (defconst proof-tactics-name-face proof-tactics-name-face509,18863 (defface proof-error-face proof-error-face514,19087 (defface proof-warning-faceproof-warning-face522,19294 (defface proof-eager-annotation-faceproof-eager-annotation-face531,19551 (defface proof-debug-message-faceproof-debug-message-face539,19769 (defface proof-boring-faceproof-boring-face547,19968 (defface proof-mouse-highlight-faceproof-mouse-highlight-face555,20160 (defface proof-highlight-dependent-faceproof-highlight-dependent-face563,20356 (defface proof-highlight-dependency-faceproof-highlight-dependency-face571,20565 (defgroup prover-config prover-config589,20824 (defcustom proof-mode-for-shell proof-mode-for-shell623,21943 (defcustom proof-mode-for-response proof-mode-for-response630,22190 (defcustom proof-mode-for-goals proof-mode-for-goals637,22473 (defcustom proof-mode-for-script proof-mode-for-script644,22728 (defcustom proof-guess-command-line proof-guess-command-line655,23162 (defcustom proof-assistant-home-page proof-assistant-home-page670,23659 (defcustom proof-context-command proof-context-command676,23829 (defcustom proof-info-command proof-info-command681,23963 (defcustom proof-showproof-command proof-showproof-command688,24235 (defcustom proof-goal-command proof-goal-command693,24371 (defcustom proof-save-command proof-save-command701,24669 (defcustom proof-find-theorems-command proof-find-theorems-command709,24979 (defconst proof-toolbar-entries-defaultproof-toolbar-entries-default716,25288 (defpgcustom toolbar-entries toolbar-entries747,27020 (defcustom proof-assistant-true-value proof-assistant-true-value765,27741 (defcustom proof-assistant-false-value proof-assistant-false-value771,27931 (defcustom proof-assistant-format-int-fn proof-assistant-format-int-fn777,28125 (defcustom proof-assistant-format-string-fn proof-assistant-format-string-fn784,28374 (defcustom proof-assistant-setting-format proof-assistant-setting-format791,28641 (defgroup proof-script proof-script813,29336 (defcustom proof-terminal-char proof-terminal-char818,29466 (defcustom proof-script-sexp-commands proof-script-sexp-commands828,29870 (defcustom proof-script-command-end-regexp proof-script-command-end-regexp839,30340 (defcustom proof-script-command-start-regexp proof-script-command-start-regexp857,31159 (defcustom proof-script-use-old-parser proof-script-use-old-parser868,31621 (defcustom proof-script-integral-proofs proof-script-integral-proofs880,32110 (defcustom proof-script-fly-past-comments proof-script-fly-past-comments895,32766 (defcustom proof-script-parse-function proof-script-parse-function902,33083 (defcustom proof-script-comment-start proof-script-comment-start920,33729 (defcustom proof-script-comment-start-regexp proof-script-comment-start-regexp931,34164 (defcustom proof-script-comment-end proof-script-comment-end939,34481 (defcustom proof-script-comment-end-regexp proof-script-comment-end-regexp951,34899 (defcustom pg-insert-output-as-comment-fn pg-insert-output-as-comment-fn959,35210 (defcustom proof-string-start-regexp proof-string-start-regexp965,35462 (defcustom proof-string-end-regexp proof-string-end-regexp970,35627 (defcustom proof-case-fold-search proof-case-fold-search975,35788 (defcustom proof-save-command-regexp proof-save-command-regexp984,36204 (defcustom proof-save-with-hole-regexp proof-save-with-hole-regexp989,36315 (defcustom proof-save-with-hole-result proof-save-with-hole-result1001,36767 (defcustom proof-goal-command-regexp proof-goal-command-regexp1012,37231 (defcustom proof-goal-with-hole-regexp proof-goal-with-hole-regexp1021,37623 (defcustom proof-goal-with-hole-result proof-goal-with-hole-result1033,38067 (defcustom proof-non-undoables-regexp proof-non-undoables-regexp1043,38466 (defcustom proof-nested-undo-regexp proof-nested-undo-regexp1054,38922 (defcustom proof-ignore-for-undo-count proof-ignore-for-undo-count1070,39634 (defcustom proof-script-next-entity-regexps proof-script-next-entity-regexps1078,39937 (defcustom proof-script-find-next-entity-fnproof-script-find-next-entity-fn1122,41671 (defcustom proof-script-imenu-generic-expression proof-script-imenu-generic-expression1142,42501 (defcustom proof-goal-command-p proof-goal-command-p1157,43162 (defcustom proof-really-save-command-p proof-really-save-command-p1184,44598 (defcustom proof-completed-proof-behaviour proof-completed-proof-behaviour1196,45059 (defcustom proof-count-undos-fn proof-count-undos-fn1224,46419 (defconst proof-no-command proof-no-command1259,48020 (defcustom proof-find-and-forget-fn proof-find-and-forget-fn1264,48224 (defcustom proof-forget-id-command proof-forget-id-command1281,48935 (defcustom pg-topterm-goalhyp-fn pg-topterm-goalhyp-fn1291,49293 (defcustom proof-kill-goal-command proof-kill-goal-command1303,49774 (defcustom proof-undo-n-times-cmd proof-undo-n-times-cmd1317,50284 (defcustom proof-nested-goals-history-p proof-nested-goals-history-p1331,50833 (defcustom proof-state-preserving-p proof-state-preserving-p1340,51171 (defcustom proof-activate-scripting-hook proof-activate-scripting-hook1350,51641 (defcustom proof-deactivate-scripting-hook proof-deactivate-scripting-hook1369,52419 (defcustom proof-indent proof-indent1382,52784 (defcustom proof-indent-pad-eol proof-indent-pad-eol1388,52958 (defcustom proof-indent-hang proof-indent-hang1395,53198 (defcustom proof-indent-enclose-offset proof-indent-enclose-offset1400,53324 (defcustom proof-indent-open-offset proof-indent-open-offset1405,53466 (defcustom proof-indent-close-offset proof-indent-close-offset1410,53603 (defcustom proof-indent-any-regexp proof-indent-any-regexp1415,53741 (defcustom proof-indent-inner-regexp proof-indent-inner-regexp1420,53901 (defcustom proof-indent-enclose-regexp proof-indent-enclose-regexp1425,54055 (defcustom proof-indent-open-regexp proof-indent-open-regexp1430,54209 (defcustom proof-indent-close-regexp proof-indent-close-regexp1435,54361 (defcustom proof-script-font-lock-keywords proof-script-font-lock-keywords1441,54515 (defcustom proof-script-syntax-table-entries proof-script-syntax-table-entries1449,54838 (defcustom proof-script-span-context-menu-extensions proof-script-span-context-menu-extensions1467,55235 (defgroup proof-shell proof-shell1493,56024 (defcustom proof-prog-name proof-prog-name1503,56195 (defcustom proof-shell-auto-terminate-commands proof-shell-auto-terminate-commands1512,56550 (defcustom proof-shell-pre-sync-init-cmd proof-shell-pre-sync-init-cmd1521,56947 (defcustom proof-shell-init-cmd proof-shell-init-cmd1535,57506 (defcustom proof-shell-restart-cmd proof-shell-restart-cmd1546,57976 (defcustom proof-shell-quit-cmd proof-shell-quit-cmd1551,58131 (defcustom proof-shell-quit-timeout proof-shell-quit-timeout1556,58298 (defcustom proof-shell-cd-cmd proof-shell-cd-cmd1566,58746 (defcustom proof-shell-start-silent-cmd proof-shell-start-silent-cmd1583,59413 (defcustom proof-shell-stop-silent-cmd proof-shell-stop-silent-cmd1592,59789 (defcustom proof-shell-silent-threshold proof-shell-silent-threshold1601,60126 (defcustom proof-shell-inform-file-processed-cmd proof-shell-inform-file-processed-cmd1609,60460 (defcustom proof-shell-inform-file-retracted-cmd proof-shell-inform-file-retracted-cmd1630,61383 (defcustom proof-auto-multiple-files proof-auto-multiple-files1658,62654 (defcustom proof-cannot-reopen-processed-files proof-cannot-reopen-processed-files1673,63375 (defcustom proof-shell-require-command-regexp proof-shell-require-command-regexp1687,64042 (defcustom proof-done-advancing-require-function proof-done-advancing-require-function1698,64504 (defcustom proof-shell-prompt-pattern proof-shell-prompt-pattern1716,64877 (defcustom proof-shell-wakeup-char proof-shell-wakeup-char1726,65299 (defcustom proof-shell-annotated-prompt-regexp proof-shell-annotated-prompt-regexp1732,65530 (defcustom proof-shell-abort-goal-regexp proof-shell-abort-goal-regexp1748,66170 (defcustom proof-shell-error-regexp proof-shell-error-regexp1753,66305 (defcustom proof-shell-truncate-before-error proof-shell-truncate-before-error1773,67099 (defcustom pg-next-error-regexp pg-next-error-regexp1787,67642 (defcustom pg-next-error-filename-regexp pg-next-error-filename-regexp1802,68252 (defcustom pg-next-error-extract-filename pg-next-error-extract-filename1826,69290 (defcustom proof-shell-interrupt-regexp proof-shell-interrupt-regexp1833,69533 (defcustom proof-shell-proof-completed-regexp proof-shell-proof-completed-regexp1847,70125 (defcustom proof-shell-clear-response-regexp proof-shell-clear-response-regexp1860,70633 (defcustom proof-shell-clear-goals-regexp proof-shell-clear-goals-regexp1867,70932 (defcustom proof-shell-start-goals-regexp proof-shell-start-goals-regexp1874,71225 (defcustom proof-shell-end-goals-regexp proof-shell-end-goals-regexp1882,71592 (defcustom proof-shell-eager-annotation-start proof-shell-eager-annotation-start1888,71834 (defcustom proof-shell-eager-annotation-start-length proof-shell-eager-annotation-start-length1906,72572 (defcustom proof-shell-eager-annotation-end proof-shell-eager-annotation-end1917,72999 (defcustom proof-shell-assumption-regexp proof-shell-assumption-regexp1933,73675 (defcustom proof-shell-process-file proof-shell-process-file1943,74087 (defcustom proof-shell-retract-files-regexp proof-shell-retract-files-regexp1965,75039 (defcustom proof-shell-compute-new-files-list proof-shell-compute-new-files-list1974,75375 (defcustom pg-use-specials-for-fontify pg-use-specials-for-fontify1986,75920 (defcustom proof-shell-set-elisp-variable-regexp proof-shell-set-elisp-variable-regexp1994,76244 (defcustom proof-shell-match-pgip-cmd proof-shell-match-pgip-cmd2027,77716 (defcustom proof-shell-issue-pgip-cmd proof-shell-issue-pgip-cmd2036,78046 (defcustom proof-shell-query-dependencies-cmd proof-shell-query-dependencies-cmd2045,78402 (defcustom proof-shell-theorem-dependency-list-regexp proof-shell-theorem-dependency-list-regexp2052,78662 (defcustom proof-shell-theorem-dependency-list-split proof-shell-theorem-dependency-list-split2068,79322 (defcustom proof-shell-show-dependency-cmd proof-shell-show-dependency-cmd2077,79747 (defcustom proof-shell-identifier-under-mouse-cmd proof-shell-identifier-under-mouse-cmd2084,80016 (defcustom proof-shell-trace-output-regexp proof-shell-trace-output-regexp2107,81097 (defcustom proof-shell-thms-output-regexp proof-shell-thms-output-regexp2123,81641 (defcustom proof-shell-filename-escapes proof-shell-filename-escapes2135,82026 (defcustom proof-shell-process-connection-type proof-shell-process-connection-type2152,82706 (defcustom proof-shell-strip-crs-from-input proof-shell-strip-crs-from-input2172,83584 (defcustom proof-shell-strip-crs-from-output proof-shell-strip-crs-from-output2184,84073 (defcustom proof-shell-insert-hook proof-shell-insert-hook2192,84441 (defcustom proof-pre-shell-start-hook proof-pre-shell-start-hook2232,86405 (defcustom proof-shell-handle-delayed-output-hookproof-shell-handle-delayed-output-hook2248,86877 (defcustom proof-shell-handle-error-or-interrupt-hookproof-shell-handle-error-or-interrupt-hook2254,87092 (defcustom proof-shell-pre-interrupt-hookproof-shell-pre-interrupt-hook2269,87706 (defcustom proof-shell-process-output-system-specific proof-shell-process-output-system-specific2279,88076 (defcustom proof-state-change-hook proof-state-change-hook2298,88941 (defcustom proof-shell-font-lock-keywords proof-shell-font-lock-keywords2309,89323 (defcustom proof-shell-syntax-table-entries proof-shell-syntax-table-entries2317,89651 (defgroup proof-goals proof-goals2335,90023 (defcustom pg-subterm-first-special-char pg-subterm-first-special-char2340,90144 (defcustom pg-subterm-anns-use-stack pg-subterm-anns-use-stack2348,90456 (defcustom pg-goals-change-goal pg-goals-change-goal2357,90760 (defcustom pbp-goal-command pbp-goal-command2362,90875 (defcustom pbp-hyp-command pbp-hyp-command2367,91031 (defcustom pg-subterm-help-cmd pg-subterm-help-cmd2372,91193 (defcustom pg-goals-error-regexp pg-goals-error-regexp2379,91429 (defcustom proof-shell-result-start proof-shell-result-start2384,91589 (defcustom proof-shell-result-end proof-shell-result-end2390,91823 (defcustom pg-subterm-start-char pg-subterm-start-char2396,92036 (defcustom pg-subterm-sep-char pg-subterm-sep-char2410,92618 (defcustom pg-subterm-end-char pg-subterm-end-char2416,92797 (defcustom pg-topterm-char pg-topterm-char2422,92954 (defcustom proof-goals-font-lock-keywords proof-goals-font-lock-keywords2439,93560 (defcustom proof-resp-font-lock-keywords proof-resp-font-lock-keywords2453,94239 (defcustom pg-before-fontify-output-hook pg-before-fontify-output-hook2465,94817 (defcustom pg-after-fontify-output-hook pg-after-fontify-output-hook2473,95177 (defgroup proof-x-symbol proof-x-symbol2485,95431 (defcustom proof-xsym-extra-modes proof-xsym-extra-modes2490,95559 (defcustom proof-xsym-font-lock-keywords proof-xsym-font-lock-keywords2503,96188 (defcustom proof-xsym-activate-command proof-xsym-activate-command2511,96565 (defcustom proof-xsym-deactivate-command proof-xsym-deactivate-command2518,96801 (defpgcustom x-symbol-language x-symbol-language2525,97043 (defpgcustom favourites favourites2540,97490 (defpgcustom menu-entries menu-entries2545,97680 (defpgcustom help-menu-entries help-menu-entries2552,97917 (defpgcustom keymap keymap2559,98180 (defpgcustom completion-table completion-table2564,98351 (defpgcustom tags-program tags-program2574,98716 (defcustom proof-general-name proof-general-name2586,98889 (defcustom proof-general-home-pageproof-general-home-page2591,99046 (defcustom proof-unnamed-theorem-nameproof-unnamed-theorem-name2597,99205 (defcustom proof-universal-keysproof-universal-keys2605,99481 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,1014 (defvar proof-included-files-list proof-included-files-list43,1171 (defvar proof-script-buffer proof-script-buffer66,2186 (defvar proof-previous-script-buffer proof-previous-script-buffer70,2326 (defvar proof-shell-buffer proof-shell-buffer75,2580 (defvar proof-goals-buffer proof-goals-buffer78,2666 (defvar proof-response-buffer proof-response-buffer81,2721 (defvar proof-trace-buffer proof-trace-buffer84,2782 (defvar proof-thms-buffer proof-thms-buffer88,2936 (defvar proof-shell-error-or-interrupt-seen proof-shell-error-or-interrupt-seen92,3091 (defvar proof-shell-proof-completed proof-shell-proof-completed97,3316 (defvar proof-terminal-string proof-terminal-string109,3861 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-favourite548,19534 (defvar proof-make-favourite-cmd-history proof-make-favourite-cmd-history571,20509 (defvar proof-make-favourite-menu-history proof-make-favourite-menu-history574,20594 (defun proof-save-favourites proof-save-favourites577,20680 (defun proof-del-favourite proof-del-favourite582,20828 (defun proof-read-favourite proof-read-favourite599,21389 (defun proof-add-favourite proof-add-favourite624,22192 (defvar proof-assistant-settings proof-assistant-settings651,23243 (defvar proof-menu-settings proof-menu-settings658,23606 (defun proof-menu-define-settings-menu proof-menu-define-settings-menu661,23680 (defun proof-menu-entry-name proof-menu-entry-name679,24324 (defun proof-menu-entry-for-setting proof-menu-entry-for-setting684,24483 (defun proof-settings-vars proof-settings-vars702,24973 (defun proof-settings-changed-from-defaults-p proof-settings-changed-from-defaults-p707,25150 (defun proof-settings-changed-from-saved-p proof-settings-changed-from-saved-p711,25256 (defun proof-settings-save proof-settings-save715,25359 (defun proof-settings-reset proof-settings-reset720,25526 (defun proof-defpacustom-fn proof-defpacustom-fn728,25772 (defmacro defpacustom defpacustom793,28165 (defun proof-assistant-invisible-command-ifposs proof-assistant-invisible-command-ifposs804,28805 (defun proof-maybe-askprefs proof-maybe-askprefs826,29780 (defun proof-assistant-settings-cmd proof-assistant-settings-cmd833,29984 (defun proof-assistant-format proof-assistant-format850,30644 (defvar proof-assistant-format-table proof-assistant-format-table867,31386 (defun proof-assistant-format-bool proof-assistant-format-bool875,31755 (defun proof-assistant-format-int proof-assistant-format-int878,31868 (defun proof-assistant-format-string proof-assistant-format-string881,31960 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-window459,16352 (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-window470,16833 (defun proof-end-of-locked-visible-p proof-end-of-locked-visible-p484,17486 (defun proof-goto-end-of-queue-or-locked-if-not-visible proof-goto-end-of-queue-or-locked-if-not-visible493,17937 (defvar pg-idioms pg-idioms512,18587 (defvar pg-visibility-specs pg-visibility-specs515,18683 (deflocal pg-script-portions pg-script-portions520,18890 (defun pg-clear-script-portions pg-clear-script-portions523,19012 (defun pg-add-script-element pg-add-script-element541,19676 (defun pg-remove-script-element pg-remove-script-element544,19752 (defsubst pg-visname pg-visname552,20030 (defun pg-add-element pg-add-element556,20175 (defun pg-open-invisible-span pg-open-invisible-span590,21804 (defun pg-remove-element pg-remove-element601,22167 (defun pg-make-element-invisible pg-make-element-invisible608,22437 (defun pg-make-element-visible pg-make-element-visible614,22694 (defun pg-toggle-element-visibility pg-toggle-element-visibility619,22873 (defun pg-redisplay-for-gnuemacs pg-redisplay-for-gnuemacs627,23203 (defun pg-show-all-portions pg-show-all-portions634,23474 (defun pg-show-all-proofs pg-show-all-proofs652,24145 (defun pg-hide-all-proofs pg-hide-all-proofs657,24273 (defun pg-add-proof-element pg-add-proof-element662,24404 (defun pg-span-name pg-span-name676,25024 (defun pg-set-span-helphighlights pg-set-span-helphighlights697,25731 (defun proof-complete-buffer-atomic proof-complete-buffer-atomic722,26555 (defun proof-register-possibly-new-processed-file proof-register-possibly-new-processed-file763,28470 (defun proof-inform-prover-file-retracted proof-inform-prover-file-retracted814,30598 (defun proof-auto-retract-dependencies proof-auto-retract-dependencies833,31384 (defun proof-unregister-buffer-file-name proof-unregister-buffer-file-name887,33924 (defun proof-protected-process-or-retract proof-protected-process-or-retract933,35747 (defun proof-deactivate-scripting-auto proof-deactivate-scripting-auto960,36917 (defun proof-deactivate-scripting proof-deactivate-scripting969,37275 (defun proof-activate-scripting proof-activate-scripting1106,42680 (defun proof-toggle-active-scripting proof-toggle-active-scripting1234,48434 (defun proof-done-advancing proof-done-advancing1275,49795 (defun proof-done-advancing-comment proof-done-advancing-comment1360,53200 (defun proof-done-advancing-save proof-done-advancing-save1379,53942 (defun proof-make-goalsave proof-make-goalsave1472,57555 (defun proof-get-name-from-goal proof-get-name-from-goal1487,58298 (defun proof-done-advancing-autosave proof-done-advancing-autosave1506,59324 (defun proof-done-advancing-other proof-done-advancing-other1570,61841 (defun proof-segment-up-to-parser proof-segment-up-to-parser1598,62821 (defun proof-script-generic-parse-find-comment-end proof-script-generic-parse-find-comment-end1661,64897 (defun proof-script-generic-parse-cmdend proof-script-generic-parse-cmdend1670,65313 (defun proof-script-generic-parse-cmdstart proof-script-generic-parse-cmdstart1695,66208 (defun proof-script-generic-parse-sexp proof-script-generic-parse-sexp1758,68916 (defun proof-cmdstart-add-segment-for-cmd proof-cmdstart-add-segment-for-cmd1782,69852 (defun proof-segment-up-to-cmdstart proof-segment-up-to-cmdstart1834,72051 (defun proof-segment-up-to-cmdend proof-segment-up-to-cmdend1895,74411 (defun proof-semis-to-vanillas proof-semis-to-vanillas1966,77056 (defun proof-script-new-command-advance proof-script-new-command-advance2005,78382 (defun proof-script-next-command-advance proof-script-next-command-advance2047,80123 (defun proof-assert-until-point-interactive proof-assert-until-point-interactive2059,80564 (defun proof-assert-until-point proof-assert-until-point2085,81686 (defun proof-assert-next-commandproof-assert-next-command2138,84118 (defun proof-goto-point proof-goto-point2186,86381 (defun proof-insert-pbp-command proof-insert-pbp-command2203,86907 (defun proof-done-retracting proof-done-retracting2235,87980 (defun proof-setup-retract-action proof-setup-retract-action2262,89091 (defun proof-last-goal-or-goalsave proof-last-goal-or-goalsave2272,89574 (defun proof-retract-target proof-retract-target2296,90443 (defun proof-retract-until-point-interactive proof-retract-until-point-interactive2381,94084 (defun proof-retract-until-point proof-retract-until-point2389,94469 (define-derived-mode proof-mode proof-mode2434,96330 (defun proof-script-set-visited-file-name proof-script-set-visited-file-name2470,97816 (defun proof-script-set-buffer-hooks proof-script-set-buffer-hooks2494,98818 (defun proof-script-kill-buffer-fn proof-script-kill-buffer-fn2504,99314 (defun proof-config-done-related proof-config-done-related2548,101136 (defun proof-generic-goal-command-p proof-generic-goal-command-p2618,103702 (defun proof-generic-state-preserving-p proof-generic-state-preserving-p2622,103877 (defun proof-generic-count-undos proof-generic-count-undos2631,104394 (defun proof-generic-find-and-forget proof-generic-find-and-forget2660,105424 (defconst proof-script-important-settingsproof-script-important-settings2711,107249 (defun proof-config-done proof-config-done2724,107786 (defun proof-setup-parsing-mechanism proof-setup-parsing-mechanism2821,111334 (defun proof-setup-imenu proof-setup-imenu2865,113187 (defun proof-setup-func-menu proof-setup-func-menu2882,113792 generic/proof-shell.el,5288 (defvar proof-shell-last-output proof-shell-last-output19,458 (defvar proof-marker proof-marker63,1714 (defvar proof-action-list proof-action-list66,1811 (defvar proof-shell-silent proof-shell-silent74,1987 (defvar proof-shell-last-prompt proof-shell-last-prompt88,2470 (defvar proof-shell-last-output-kind proof-shell-last-output-kind93,2700 (defvar proof-shell-delayed-output proof-shell-delayed-output114,3522 (defvar proof-shell-delayed-output-kind proof-shell-delayed-output-kind117,3643 (defcustom proof-shell-active-scripting-indicatorproof-shell-active-scripting-indicator126,3846 (defun proof-shell-ready-prover proof-shell-ready-prover179,5322 (defun proof-shell-live-buffer proof-shell-live-buffer193,5862 (defun proof-shell-available-p proof-shell-available-p200,6097 (defun proof-grab-lock proof-grab-lock206,6320 (defun proof-release-lock proof-release-lock223,7037 (defcustom proof-shell-fiddle-frames proof-shell-fiddle-frames243,7593 (deflocal proof-eagerly-raise proof-eagerly-raise250,7834 (defun proof-shell-start proof-shell-start253,7940 (defvar proof-shell-kill-function-hooks proof-shell-kill-function-hooks437,15128 (defun proof-shell-kill-function proof-shell-kill-function440,15226 (defun proof-shell-clear-state proof-shell-clear-state531,19076 (defun proof-shell-exit proof-shell-exit546,19519 (defun proof-shell-bail-out proof-shell-bail-out558,19964 (defun proof-shell-restart proof-shell-restart567,20441 (defvar proof-shell-no-response-display proof-shell-no-response-display609,21825 (defvar proof-shell-urgent-message-marker proof-shell-urgent-message-marker612,21929 (defvar proof-shell-urgent-message-scanner proof-shell-urgent-message-scanner615,22050 (defun proof-shell-handle-output proof-shell-handle-output619,22177 (defun proof-shell-handle-delayed-output proof-shell-handle-delayed-output693,25514 (defvar proof-shell-ignore-errors proof-shell-ignore-errors728,26936 (defun proof-shell-handle-error proof-shell-handle-error734,27138 (defun proof-shell-handle-interrupt proof-shell-handle-interrupt752,27982 (defun proof-shell-error-or-interrupt-action proof-shell-error-or-interrupt-action766,28598 (defun proof-goals-pos proof-goals-pos784,29424 (defun proof-pbp-focus-on-first-goal proof-pbp-focus-on-first-goal789,29629 (defsubst proof-shell-string-match-safe proof-shell-string-match-safe801,30164 (defun proof-shell-process-output proof-shell-process-output806,30332 (defvar proof-shell-insert-space-fudge proof-shell-insert-space-fudge917,34972 (defun proof-shell-insert proof-shell-insert926,35281 (defun proof-shell-command-queue-item proof-shell-command-queue-item994,37815 (defun proof-shell-set-silent proof-shell-set-silent999,37972 (defun proof-shell-start-silent-item proof-shell-start-silent-item1005,38191 (defun proof-shell-clear-silent proof-shell-clear-silent1011,38383 (defun proof-shell-stop-silent-item proof-shell-stop-silent-item1017,38605 (defun proof-shell-should-be-silent proof-shell-should-be-silent1024,38877 (defun proof-append-alist proof-append-alist1037,39433 (defun proof-start-queue proof-start-queue1093,41560 (defun proof-extend-queue proof-extend-queue1104,41909 (defun proof-shell-exec-loop proof-shell-exec-loop1115,42290 (defun proof-shell-insert-loopback-cmd proof-shell-insert-loopback-cmd1177,44757 (defun proof-shell-message proof-shell-message1215,46480 (defun proof-shell-process-urgent-message proof-shell-process-urgent-message1221,46696 (defvar proof-shell-minibuffer-urgent-interactive-input-history proof-shell-minibuffer-urgent-interactive-input-history1432,55614 (defun proof-shell-minibuffer-urgent-interactive-input proof-shell-minibuffer-urgent-interactive-input1434,55684 (defun proof-shell-process-urgent-messages proof-shell-process-urgent-messages1446,56054 (defun proof-shell-filter proof-shell-filter1515,59110 (defun proof-shell-filter-process-output proof-shell-filter-process-output1668,65447 (defvar pg-last-tracing-output-time pg-last-tracing-output-time1721,67501 (defvar pg-tracing-slow-mode pg-tracing-slow-mode1724,67607 (defconst pg-slow-mode-duration pg-slow-mode-duration1727,67696 (defconst pg-fast-tracing-mode-threshold pg-fast-tracing-mode-threshold1730,67778 (defvar pg-tracing-cleanup-timer pg-tracing-cleanup-timer1733,67906 (defun pg-tracing-tight-loop pg-tracing-tight-loop1735,67945 (defun pg-finish-tracing-display pg-finish-tracing-display1778,69698 (defun proof-shell-dont-show-annotations proof-shell-dont-show-annotations1789,69968 (defun proof-shell-show-annotations proof-shell-show-annotations1805,70503 (defun proof-shell-wait proof-shell-wait1826,71000 (defun proof-done-invisible proof-done-invisible1846,71910 (defun proof-shell-invisible-command proof-shell-invisible-command1889,73633 (defun proof-shell-invisible-cmd-get-result proof-shell-invisible-cmd-get-result1922,74883 (defun proof-shell-invisible-command-invisible-result proof-shell-invisible-command-invisible-result1939,75564 (define-derived-mode proof-shell-mode proof-shell-mode1959,76068 (defconst proof-shell-important-settingsproof-shell-important-settings2029,78671 (defun proof-shell-config-done proof-shell-config-done2034,78771 generic/proof-site.el,1154 (defgroup proof-general proof-general20,593 (defgroup proof-general-internals proof-general-internals33,1009 (defun proof-home-directory-fn proof-home-directory-fn42,1202 (defcustom proof-home-directoryproof-home-directory53,1572 (defcustom proof-images-directoryproof-images-directory62,1938 (defcustom proof-info-directoryproof-info-directory68,2139 (defcustom proof-assistant-tableproof-assistant-table97,3388 (defun proof-string-to-list proof-string-to-list156,5375 (defcustom proof-assistants proof-assistants172,5866 (defun proof-ready-for-assistant proof-ready-for-assistant220,7691 (defconst proof-general-version proof-general-version335,11984 (defcustom proof-assistant-cusgrp proof-assistant-cusgrp350,12549 (defcustom proof-assistant-internals-cusgrp proof-assistant-internals-cusgrp358,12852 (defcustom proof-assistant proof-assistant366,13164 (defcustom proof-assistant-symbol proof-assistant-symbol374,13433 (defvar proof-running-on-XEmacs proof-running-on-XEmacs391,13981 (defvar proof-running-on-Emacs21 proof-running-on-Emacs21393,14103 (defvar proof-running-on-win32 proof-running-on-win32397,14350 generic/proof-splash.el,976 (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-msg59,1970 (defconst proof-splash-welcome proof-splash-welcome68,2349 (defun proof-get-image proof-get-image87,2913 (defvar proof-splash-timeout-conf proof-splash-timeout-conf139,4737 (defun proof-splash-centre-spaces proof-splash-centre-spaces142,4850 (defun proof-splash-remove-screen proof-splash-remove-screen170,6019 (defun proof-splash-remove-buffer proof-splash-remove-buffer191,6736 (defvar proof-splash-seen proof-splash-seen207,7400 (defun proof-splash-display-screen proof-splash-display-screen211,7517 (defun proof-splash-message proof-splash-message286,10676 (defun proof-splash-timeout-waiter proof-splash-timeout-waiter296,11039 (defun proof-splash-set-frame-titles proof-splash-set-frame-titles313,11778 generic/proof-syntax.el,1296 (defun proof-ids-to-regexp proof-ids-to-regexp16,445 (defun proof-anchor-regexp proof-anchor-regexp20,609 (defconst proof-no-regexpproof-no-regexp24,711 (defun proof-regexp-alt proof-regexp-alt29,806 (defun proof-regexp-region proof-regexp-region38,1092 (defun proof-re-search-forward-region proof-re-search-forward-region47,1515 (defun proof-re-search-forward proof-re-search-forward60,2010 (defun proof-re-search-backward proof-re-search-backward66,2271 (defun proof-string-match proof-string-match72,2535 (defun proof-string-match-safe proof-string-match-safe78,2767 (defun proof-stringfn-match proof-stringfn-match82,2972 (defun proof-looking-at proof-looking-at89,3232 (defun proof-looking-at-safe proof-looking-at-safe95,3422 (defun proof-looking-at-syntactic-context proof-looking-at-syntactic-context99,3562 (defun proof-replace-string proof-replace-string111,3894 (defun proof-replace-regexp proof-replace-regexp116,4079 (defvar proof-id proof-id124,4292 (defun proof-ids proof-ids130,4512 (defun proof-zap-commas proof-zap-commas143,5073 (defun proof-format proof-format161,5636 (defun proof-format-filename proof-format-filename180,6275 (defun proof-insert proof-insert229,7753 (defun proof-splice-separator proof-splice-separator265,8762 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,3092 (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-regexp459,16467 (defun pg-remove-specials pg-remove-specials463,16579 (defun proof-fontify-buffer proof-fontify-buffer477,17004 (defun proof-warn-if-unset proof-warn-if-unset490,17245 (defun proof-get-window-for-buffer proof-get-window-for-buffer495,17463 (defun proof-display-and-keep-buffer proof-display-and-keep-buffer532,19115 (defun proof-clean-buffer proof-clean-buffer563,20391 (defun proof-message proof-message575,20869 (defun proof-warning proof-warning580,21082 (defun proof-debug proof-debug587,21416 (defun proof-switch-to-buffer proof-switch-to-buffer600,21907 (defun proof-resize-window-tofit proof-resize-window-tofit633,23599 (defun proof-submit-bug-report proof-submit-bug-report733,27627 (defun proof-deftoggle-fn proof-deftoggle-fn756,28406 (defmacro proof-deftoggle proof-deftoggle771,29061 (defun proof-defintset-fn proof-defintset-fn778,29435 (defmacro proof-defintset proof-defintset792,30090 (defun proof-defstringset-fn proof-defstringset-fn799,30467 (defmacro proof-defstringset proof-defstringset812,31094 (defun pg-custom-save-vars pg-custom-save-vars826,31559 (defun pg-custom-reset-vars pg-custom-reset-vars844,32285 (defun proof-locate-executable proof-locate-executable857,32622 (defconst proof-extra-flsproof-extra-fls889,34035 generic/proof-x-symbol.el,960 (defvar proof-x-symbol-initialized proof-x-symbol-initialized53,2149 (defun proof-x-symbol-tokenlang-file proof-x-symbol-tokenlang-file56,2244 (defun proof-x-symbol-support-maybe-available proof-x-symbol-support-maybe-available62,2426 (defun proof-x-symbol-initialize proof-x-symbol-initialize82,3171 (defun proof-x-symbol-enable proof-x-symbol-enable177,7034 (defun proof-x-symbol-refresh-output-buffers proof-x-symbol-refresh-output-buffers199,8003 (defun proof-x-symbol-mode-associated-buffers proof-x-symbol-mode-associated-buffers214,8757 (defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region236,9461 (defun proof-x-symbol-encode-shell-input proof-x-symbol-encode-shell-input238,9527 (defun proof-x-symbol-set-language proof-x-symbol-set-language255,10118 (defun proof-x-symbol-shell-config proof-x-symbol-shell-config260,10289 (defun proof-x-symbol-config-output-buffer proof-x-symbol-config-output-buffer308,12456 generic/span.el,192 (defsubst delete-spans delete-spans22,471 (defsubst span-property-safe span-property-safe26,625 (defsubst set-span-start set-span-start30,764 (defsubst set-span-end set-span-end34,896 generic/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-buffer110,3474 (defsubst span-detached-p span-detached-p115,3566 (defsubst set-span-face set-span-face120,3678 (defsubst fold-spans fold-spans125,3774 (defsubst set-span-properties set-span-properties130,3972 (defsubst set-span-keymap set-span-keymap135,4081 (defsubst span-at-event span-at-event140,4196 generic/span-overlay.el,2198 (defvar before-list before-list20,771 (defun foldr foldr27,906 (defun foldl foldl39,1239 (defsubst span-start span-start51,1556 (defsubst span-end span-end55,1648 (defun set-span-property set-span-property59,1734 (defsubst span-property span-property63,1850 (defun span-read-only-hook span-read-only-hook67,1961 (defun span-read-only span-read-only71,2093 (defun span-read-write span-read-write86,2871 (defun span-give-warning span-give-warning92,3090 (defun span-write-warning span-write-warning96,3198 (defun int-nil-lt int-nil-lt101,3421 (defun span-lt span-lt110,3624 (defun span-traverse span-traverse115,3783 (defun add-span add-span131,4230 (defun make-span make-span145,4632 (defun remove-span remove-span149,4763 (defun spans-at-point spans-at-point162,5216 (defun append-unique append-unique176,5696 (defun spans-at-region spans-at-region179,5783 (defun spans-at-point-prop spans-at-point-prop186,6005 (defun spans-at-region-prop spans-at-region-prop194,6255 (defun span-at span-at206,6602 (defsubst detach-span detach-span212,6816 (defsubst delete-span delete-span218,6943 (defsubst set-span-endpoints set-span-endpoints226,7186 (defsubst mapcar-spans mapcar-spans233,7402 (defun map-spans-aux map-spans-aux237,7606 (defsubst map-spans map-spans241,7721 (defun find-span-aux find-span-aux244,7779 (defun find-span find-span249,7905 (defun span-at-before span-at-before252,7970 (defun prev-span prev-span265,8412 (defun next-span next-span274,8694 (defsubst span-live-p span-live-p299,9678 (defun span-raise span-raise305,9844 (defalias 'span-object span-object311,10075 (defun span-string span-string313,10116 (defun set-span-properties set-span-properties319,10298 (defun span-find-span span-find-span331,10553 (defsubst span-at-event span-at-event342,10912 (defun make-detached-span make-detached-span347,11036 (defun fold-spans-aux fold-spans-aux353,11170 (defun fold-spans fold-spans361,11426 (defsubst span-buffer span-buffer368,11634 (defsubst span-detached-p span-detached-p373,11726 (defsubst set-span-face set-span-face381,11922 (defsubst set-span-keymap set-span-keymap386,12022 generic/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,7185 (defun texi-docstring-magic-munge-docstring texi-docstring-magic-munge-docstring200,7500 (defun texi-docstring-magic-texi texi-docstring-magic-texi239,8787 (defun texi-docstring-magic-format-default texi-docstring-magic-format-default252,9227 (defun texi-docstring-magic-texi-for texi-docstring-magic-texi-for268,9862 (defconst texi-docstring-magic-commenttexi-docstring-magic-comment326,11822 (defun texi-docstring-magic texi-docstring-magic332,11976 (defun texi-docstring-magic-face-at-point texi-docstring-magic-face-at-point366,13056 (defun texi-docstring-magic-insert-magic texi-docstring-magic-insert-magic381,13579 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-found64,2062 (defun isa-set-isatool-command isa-set-isatool-command67,2175 (defun isa-shell-command-to-string isa-shell-command-to-string87,2959 (defun isa-getenv isa-getenv95,3411 (defcustom isabelle-program-name isabelle-program-name114,4068 (defvar isabelle-prog-name isabelle-prog-name140,5016 (defun isabelle-command-line isabelle-command-line143,5143 (defun isabelle-choose-logic isabelle-choose-logic166,6051 (defun isa-tool-list-logics isa-tool-list-logics188,7023 (defun isa-view-doc isa-view-doc195,7261 (defvar isabelle-version-string isabelle-version-string202,7485 (defun isa-version isa-version204,7526 (defconst isa-supports-pgip isa-supports-pgip217,8009 (defun isa-tool-list-docs isa-tool-list-docs225,8239 (defun isa-quit isa-quit243,8961 (defconst isabelle-verbatim-regexp isabelle-verbatim-regexp250,9156 (defun isabelle-verbatim isabelle-verbatim253,9297 (defcustom isabelle-refresh-logics isabelle-refresh-logics269,9888 (defcustom isabelle-logics-available isabelle-logics-available277,10215 (defcustom isabelle-chosen-logic isabelle-chosen-logic285,10515 (defconst isabelle-docs-menu isabelle-docs-menu298,10983 (defun isabelle-logics-menu-calculate isabelle-logics-menu-calculate308,11376 (defvar isabelle-time-to-refresh-logics isabelle-time-to-refresh-logics324,11885 (defun isabelle-logics-menu-refresh isabelle-logics-menu-refresh327,11978 (defun isabelle-logics-menu-filter isabelle-logics-menu-filter344,12677 (defun isabelle-menu-bar-update-logics isabelle-menu-bar-update-logics350,12887 (defvar isabelle-logics-menu-entries isabelle-logics-menu-entries361,13243 (defvar isabelle-logics-menu isabelle-logics-menu363,13315 (defun isabelle-load-isar-keywords isabelle-load-isar-keywords376,13933 (defpacustom show-types show-types403,14888 (defpacustom show-sorts show-sorts408,15004 (defpacustom show-consts show-consts413,15120 (defpacustom long-names long-names418,15254 (defpacustom eta-contract eta-contract423,15386 (defpacustom trace-simplifier trace-simplifier428,15527 (defpacustom trace-rules trace-rules433,15659 (defpacustom quick-and-dirty quick-and-dirty438,15791 (defpacustom full-proofs full-proofs443,15927 (defpacustom global-timing global-timing449,16236 (defpacustom theorem-dependencies theorem-dependencies455,16394 (defpacustom goals-limit goals-limit461,16659 (defpacustom prems-limit prems-limit466,16798 (defpacustom print-depth print-depth471,16958 (defpgdefault menu-entriesmenu-entries483,17247 (defpgdefault help-menu-entries help-menu-entries490,17409 (defpgdefault x-symbol-language x-symbol-language498,17603 (defun isabelle-convert-idmarkup-to-subterm isabelle-convert-idmarkup-to-subterm521,18218 (defun isabelle-create-span-menu isabelle-create-span-menu546,19257 (defun isabelle-xml-sml-escapes isabelle-xml-sml-escapes563,19751 (defun isabelle-process-pgip isabelle-process-pgip566,19852 (defun isabelle-parse-syntax-dump isabelle-parse-syntax-dump583,20438 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-config593,22373 (defun isa-response-mode-config isa-response-mode-config600,22622 (defun isa-goals-mode-config isa-goals-mode-config605,22783 (defun isa-preprocessing isa-preprocessing613,23107 (defpgdefault completion-tablecompletion-table627,23611 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.el,1883 (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,10961 (defun isar-shell-compute-new-files-list isar-shell-compute-new-files-list306,11324 (defun isar-activate-scripting isar-activate-scripting317,11790 (define-derived-mode isar-shell-mode isar-shell-mode326,11960 (define-derived-mode isar-response-mode isar-response-mode331,12083 (define-derived-mode isar-goals-mode isar-goals-mode336,12265 (define-derived-mode isar-mode isar-mode341,12440 (defpgdefault menu-entriesmenu-entries374,13796 (defun isar-count-undos isar-count-undos398,14818 (defun isar-find-and-forget isar-find-and-forget424,15919 (defun isar-goal-command-p isar-goal-command-p471,17764 (defun isar-global-save-command-p isar-global-save-command-p475,17896 (defvar isar-current-goal isar-current-goal496,18733 (defun isar-state-preserving-p isar-state-preserving-p499,18799 (defvar isar-shell-current-line-width isar-shell-current-line-width522,19833 (defun isar-shell-adjust-line-width isar-shell-adjust-line-width528,20051 (defun isar-pre-shell-start isar-pre-shell-start548,20934 (defun isar-preprocessing isar-preprocessing560,21270 (defun isar-mode-config isar-mode-config583,22481 (defun isar-shell-mode-config isar-shell-mode-config594,22984 (defun isar-response-mode-config isar-response-mode-config605,23354 (defun isar-goals-mode-config isar-goals-mode-config614,23611 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,4918 (defconst isar-script-syntax-table-entries isar-script-syntax-table-entries18,414 (defconst isar-script-syntax-table-alistisar-script-syntax-table-alist57,1326 (defun isar-init-syntax-table isar-init-syntax-table66,1609 (defun isar-init-output-syntax-table isar-init-output-syntax-table74,1857 (defconst isar-keywords-theory-encloseisar-keywords-theory-enclose89,2272 (defconst isar-keywords-theoryisar-keywords-theory94,2424 (defconst isar-keywords-saveisar-keywords-save99,2569 (defconst isar-keywords-proof-encloseisar-keywords-proof-enclose104,2698 (defconst isar-keywords-proofisar-keywords-proof110,2880 (defconst isar-keywords-proof-contextisar-keywords-proof-context117,3078 (defconst isar-keywords-local-goalisar-keywords-local-goal121,3192 (defconst isar-keywords-improperisar-keywords-improper125,3304 (defconst isar-keywords-outlineisar-keywords-outline130,3443 (defconst isar-keywords-fumeisar-keywords-fume133,3508 (defconst isar-keywords-indent-openisar-keywords-indent-open140,3726 (defconst isar-keywords-indent-closeisar-keywords-indent-close146,3910 (defconst isar-keywords-indent-encloseisar-keywords-indent-enclose150,4015 (defun isar-regexp-simple-alt isar-regexp-simple-alt158,4194 (defun isar-ids-to-regexp isar-ids-to-regexp178,4955 (defconst isar-ext-first isar-ext-first212,6223 (defconst isar-ext-rest isar-ext-rest213,6290 (defconst isar-long-id-stuff isar-long-id-stuff215,6362 (defconst isar-id isar-id216,6436 (defconst isar-idx isar-idx217,6506 (defconst isar-string isar-string219,6565 (defconst isar-any-command-regexpisar-any-command-regexp221,6627 (defconst isar-name-regexpisar-name-regexp225,6761 (defconst isar-tac-regexpisar-tac-regexp229,6930 (defconst isar-save-command-regexpisar-save-command-regexp233,7038 (defconst isar-global-save-command-regexpisar-global-save-command-regexp236,7139 (defconst isar-goal-command-regexpisar-goal-command-regexp239,7253 (defconst isar-local-goal-command-regexpisar-local-goal-command-regexp242,7361 (defconst isar-comment-start isar-comment-start245,7474 (defconst isar-comment-end isar-comment-end246,7509 (defconst isar-comment-start-regexp isar-comment-start-regexp247,7542 (defconst isar-comment-end-regexp isar-comment-end-regexp248,7613 (defconst isar-string-start-regexp isar-string-start-regexp250,7681 (defconst isar-string-end-regexp isar-string-end-regexp251,7729 (defconst isar-antiq-regexpisar-antiq-regexp260,7979 (defface isabelle-class-name-faceisabelle-class-name-face267,8159 (defface isabelle-tfree-name-faceisabelle-tfree-name-face277,8434 (defface isabelle-tvar-name-faceisabelle-tvar-name-face287,8715 (defface isabelle-free-name-faceisabelle-free-name-face297,8995 (defface isabelle-bound-name-faceisabelle-bound-name-face307,9271 (defface isabelle-var-name-faceisabelle-var-name-face317,9550 (defconst isabelle-class-name-face isabelle-class-name-face327,9829 (defconst isabelle-tfree-name-face isabelle-tfree-name-face328,9891 (defconst isabelle-tvar-name-face isabelle-tvar-name-face329,9953 (defconst isabelle-free-name-face isabelle-free-name-face330,10014 (defconst isabelle-bound-name-face isabelle-bound-name-face331,10075 (defconst isabelle-var-name-face isabelle-var-name-face332,10137 (defvar isar-font-lock-keywords-1isar-font-lock-keywords-1334,10198 (defvar isar-output-font-lock-keywords-1isar-output-font-lock-keywords-1348,11127 (defvar isar-goals-font-lock-keywordsisar-goals-font-lock-keywords360,11783 (defconst isar-undo isar-undo391,12417 (defconst isar-kill isar-kill392,12479 (defun isar-remove isar-remove394,12509 (defun isar-undos isar-undos397,12588 (defun isar-cannot-undo isar-cannot-undo401,12694 (defconst isar-undo-fail-regexpisar-undo-fail-regexp405,12765 (defconst isar-undo-skip-regexpisar-undo-skip-regexp409,12903 (defconst isar-undo-ignore-regexpisar-undo-ignore-regexp412,13024 (defconst isar-undo-remove-regexpisar-undo-remove-regexp415,13089 (defconst isar-undo-kill-regexpisar-undo-kill-regexp420,13229 (defconst isar-any-entity-regexpisar-any-entity-regexp426,13371 (defconst isar-named-entity-regexpisar-named-entity-regexp431,13558 (defconst isar-unnamed-entity-regexpisar-unnamed-entity-regexp436,13735 (defconst isar-next-entity-regexpsisar-next-entity-regexps439,13837 (defconst isar-generic-expressionisar-generic-expression447,14144 (defconst isar-indent-any-regexpisar-indent-any-regexp458,14378 (defconst isar-indent-inner-regexpisar-indent-inner-regexp460,14471 (defconst isar-indent-enclose-regexpisar-indent-enclose-regexp462,14537 (defconst isar-indent-open-regexpisar-indent-open-regexp464,14653 (defconst isar-indent-close-regexpisar-indent-close-regexp466,14763 (defconst isar-outline-regexpisar-outline-regexp472,14900 (defconst isar-outline-heading-end-regexp isar-outline-heading-end-regexp476,15053 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 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 phox/phox.el,886 (defcustom phox-prog-name phox-prog-name30,907 (defcustom phox-sym-lock phox-sym-lock35,1009 (defcustom phox-web-pagephox-web-page40,1107 (defcustom phox-doc-dir phox-doc-dir46,1257 (defcustom phox-lib-dir phox-lib-dir52,1405 (defcustom phox-tags-program phox-tags-program58,1549 (defcustom phox-tags-doc phox-tags-doc64,1729 (defcustom phox-etags phox-etags70,1867 (defpgdefault menu-entriesmenu-entries90,2297 (defun phox-config phox-config107,2626 (defun phox-shell-config phox-shell-config149,4550 (define-derived-mode phox-mode phox-mode189,6130 (define-derived-mode phox-shell-mode phox-shell-mode204,6574 (define-derived-mode phox-response-mode phox-response-mode209,6702 (define-derived-mode phox-goals-mode phox-goals-mode221,7121 (defun phox-pre-shell-start phox-pre-shell-start247,8180 (defpgdefault completion-tablecompletion-table261,8694 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,196 (defconst phox-font-lock-keywordsphox-font-lock-keywords6,282 (defconst phox-sym-lock-keywords-tablephox-sym-lock-keywords-table66,2407 (defun phox-sym-lock-start phox-sym-lock-start89,2988 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-outline.el,108 (defun phox-outline-level(phox-outline-level32,1113 (defun phox-setup-outline phox-setup-outline46,1587 phox/phox-sym-lock.el,2167 (defvar phox-sym-lock-sym-count phox-sym-lock-sym-count34,1669 (defvar phox-sym-lock-ext-start phox-sym-lock-ext-start37,1739 (defvar phox-sym-lock-ext-end phox-sym-lock-ext-end39,1861 (defvar phox-sym-lock-font-size phox-sym-lock-font-size42,1980 (defvar phox-sym-lock-keywords phox-sym-lock-keywords47,2170 (defvar phox-sym-lock-enabled phox-sym-lock-enabled52,2346 (defvar phox-sym-lock-color phox-sym-lock-color57,2508 (defvar phox-sym-lock-mouse-face phox-sym-lock-mouse-face62,2726 (defvar phox-sym-lock-mouse-face-enabled phox-sym-lock-mouse-face-enabled67,2916 (defconst phox-sym-lock-with-mule phox-sym-lock-with-mule72,3106 (defun phox-sym-lock-gen-symbol phox-sym-lock-gen-symbol75,3190 (defun phox-sym-lock-make-symbols-atomic phox-sym-lock-make-symbols-atomic83,3493 (defun phox-sym-lock-compute-font-size phox-sym-lock-compute-font-size110,4435 (defvar phox-sym-lock-font-namephox-sym-lock-font-name147,5781 (defun phox-sym-lock-set-foreground phox-sym-lock-set-foreground185,7066 (defun phox-sym-lock-translate-char phox-sym-lock-translate-char199,7675 (defun phox-sym-lock-translate-char-or-string phox-sym-lock-translate-char-or-string207,7943 (defun phox-sym-lock-remap-face phox-sym-lock-remap-face214,8170 (defvar phox-sym-lock-clear-facephox-sym-lock-clear-face234,9160 (defun phox-sym-lock phox-sym-lock246,9582 (defun phox-sym-lock-rec phox-sym-lock-rec255,9986 (defun phox-sym-lock-atom-face phox-sym-lock-atom-face261,10139 (defun phox-sym-lock-pre-idle-hook-first phox-sym-lock-pre-idle-hook-first266,10435 (defun phox-sym-lock-pre-idle-hook-last phox-sym-lock-pre-idle-hook-last274,10793 (defun phox-sym-lock-enable phox-sym-lock-enable283,11168 (defun phox-sym-lock-disable phox-sym-lock-disable296,11581 (defun phox-sym-lock-mouse-face-enable phox-sym-lock-mouse-face-enable309,11999 (defun phox-sym-lock-mouse-face-disable phox-sym-lock-mouse-face-disable316,12214 (defun phox-sym-lock-font-lock-hook phox-sym-lock-font-lock-hook323,12433 (defun font-lock-set-defaults font-lock-set-defaults338,13126 (defun phox-sym-lock-patch-keywords phox-sym-lock-patch-keywords349,13504 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,2672 (defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts21,705 (defvar x-symbol-phox-name x-symbol-phox-name31,1204 (defvar x-symbol-phox-modeline-name x-symbol-phox-modeline-name32,1246 (defcustom x-symbol-phox-header-groups-alist x-symbol-phox-header-groups-alist34,1291 (defcustom x-symbol-phox-electric-ignore x-symbol-phox-electric-ignore41,1511 (defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts48,1759 (defvar x-symbol-phox-extra-menu-items x-symbol-phox-extra-menu-items51,1860 (defvar x-symbol-phox-token-grammarx-symbol-phox-token-grammar55,1950 (defvar x-symbol-phox-input-token-grammarx-symbol-phox-input-token-grammar66,2456 (defun x-symbol-phox-default-token-list x-symbol-phox-default-token-list72,2711 (defvar x-symbol-phox-user-table x-symbol-phox-user-table84,3000 (defvar x-symbol-phox-generated-data x-symbol-phox-generated-data87,3109 (defvar x-symbol-phox-master-directory x-symbol-phox-master-directory95,3348 (defvar x-symbol-phox-image-searchpath x-symbol-phox-image-searchpath96,3397 (defvar x-symbol-phox-image-cached-dirs x-symbol-phox-image-cached-dirs97,3445 (defvar x-symbol-phox-image-file-truename-alist x-symbol-phox-image-file-truename-alist98,3511 (defvar x-symbol-phox-image-keywords x-symbol-phox-image-keywords99,3564 (defcustom x-symbol-phox-class-alistx-symbol-phox-class-alist105,3784 (defcustom x-symbol-phox-class-face-alist x-symbol-phox-class-face-alist116,4166 (defvar x-symbol-phox-font-lock-keywords x-symbol-phox-font-lock-keywords126,4479 (defvar x-symbol-phox-font-lock-allowed-faces x-symbol-phox-font-lock-allowed-faces128,4526 (defvar x-symbol-phox-case-insensitive x-symbol-phox-case-insensitive134,4751 (defvar x-symbol-phox-token-shape x-symbol-phox-token-shape135,4795 (defvar x-symbol-phox-input-token-ignore x-symbol-phox-input-token-ignore136,4834 (defvar x-symbol-phox-token-list x-symbol-phox-token-list143,5073 (defvar x-symbol-phox-xsymb0-table x-symbol-phox-xsymb0-table145,5118 (defun x-symbol-phox-prepare-table x-symbol-phox-prepare-table166,5573 (defvar x-symbol-phox-tablex-symbol-phox-table173,5744 (defvar x-symbol-phox-menu-alist x-symbol-phox-menu-alist184,6116 (defvar x-symbol-phox-grid-alist x-symbol-phox-grid-alist186,6206 (defvar x-symbol-phox-decode-atree x-symbol-phox-decode-atree189,6297 (defvar x-symbol-phox-decode-alist x-symbol-phox-decode-alist191,6390 (defvar x-symbol-phox-encode-alist x-symbol-phox-encode-alist193,6487 (defvar x-symbol-phox-nomule-decode-exec x-symbol-phox-nomule-decode-exec197,6644 (defvar x-symbol-phox-nomule-encode-exec x-symbol-phox-nomule-encode-exec199,6744 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 todo,1297 function to to373,15257 $Id: todo,2,21 This is an outline file. Use C-c C-n,4,67 X 41,1156 *** C Improved configurability of command settings,172,6638 We should let command settings,173,6695 We should let command settings, etc,173,6695 - XEmacs pg forces on font-lock,323,12844 Save foo;399,16380 *** A Doc new bits: font lock keywords,469,19081 *** A Doc new bits: font lock keywords, filename %e,469,19081 Added proof-{script,470,19138 Added proof-{script,shell,470,19138 Added proof-{script,shell,goals,470,19138 Presently used only in proof-easy-config,471,19198 - Mention configuring function menus,482,19534 - document mouse functions,484,19620 - document mouse functions, proof-cd,484,19620 - document mouse functions, proof-cd, process quit timeout,484,19620 X-Symbol,485,19683 X-Symbol, prog-name-guess,485,19683 *** D Fix INFO-DIR-ENTRY in 499,20191 *** C Fixing up errors caused by pbp-generated commands; currently,565,22668 should mean generates an error. With LEGO pbp,568,22874 tactic which always succeeds,569,22938 decodes annotations eagerly. Lazily would be faster,577,23294 the tech report claims --- djs: probably not much faster,578,23363 *** 6. Update Emacs and prover versions in texi,667,26366 doc/ProofGeneral.texi,5815 @node TopTop166,5018 @node PrefacePreface203,6141 @node Latest news for 3.5Latest news for 3.5226,6729 @node FutureFuture264,8387 @node CreditsCredits299,9937 @node Introducing Proof GeneralIntroducing Proof General397,13352 @node Quick start guideQuick start guide452,15344 @node Features of Proof GeneralFeatures of Proof General506,17913 @node Supported proof assistantsSupported proof assistants595,21838 @node Prerequisites for this manualPrerequisites for this manual647,23834 @node Organization of this manualOrganization of this manual691,25460 @node Basic Script ManagementBasic Script Management717,26287 @node Walkthrough example in Isabelle/IsarWalkthrough example in Isabelle/Isar736,26892 @node Proof scriptsProof scripts963,35427 @node Script buffersScript buffers1006,37547 @node Locked queue and editing regionsLocked queue and editing regions1028,38124 @node Goal-save sequencesGoal-save sequences1084,40271 @node Active scripting bufferActive scripting buffer1121,41757 @node Summary of Proof General buffersSummary of Proof General buffers1190,45177 @node Script editing commandsScript editing commands1252,47851 @node Script processing commandsScript processing commands1329,50614 @node Proof assistant commandsProof assistant commands1457,55915 @node Toolbar commandsToolbar commands1603,60802 @node Interrupting during trace outputInterrupting during trace output1627,61731 @node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing1666,63654 @node Goals buffer commandsGoals buffer commands1680,64154 @node Advanced Script ManagementAdvanced Script Management1769,67686 @node Visibility of completed proofsVisibility of completed proofs1800,68840 @node Switching between proof scriptsSwitching between proof scripts1855,70763 @node View of processed files View of processed files 1892,72735 @node Retracting across filesRetracting across files1952,75786 @node Asserting across filesAsserting across files1965,76417 @node Automatic multiple file handlingAutomatic multiple file handling1978,76983 @node Escaping script managementEscaping script management2003,78017 @node Experimental featuresExperimental features2061,80220 @node Support for other PackagesSupport for other Packages2095,81482 @node Syntax highlightingSyntax highlighting2127,82357 @node X-Symbol supportX-Symbol support2166,83966 @node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)2225,86512 @node Support for outline modeSupport for outline mode2284,88642 @node Support for completionSupport for completion2310,89772 @node Support for tagsSupport for tags2367,91935 @node Customizing Proof GeneralCustomizing Proof General2419,94263 @node Basic optionsBasic options2459,95933 @node How to customizeHow to customize2483,96691 @node Display customizationDisplay customization2534,98781 @node User optionsUser options2659,104015 @node Changing facesChanging faces2913,113021 @node Tweaking configuration settingsTweaking configuration settings2988,115690 @node Hints and TipsHints and Tips3045,118215 @node Adding your own keybindingsAdding your own keybindings3064,118816 @node Using file variablesUsing file variables3120,121349 @node Using abbreviationsUsing abbreviations3173,123172 @node LEGO Proof GeneralLEGO Proof General3212,124587 @node LEGO specific commandsLEGO specific commands3253,125956 @node LEGO tagsLEGO tags3273,126411 @node LEGO customizationsLEGO customizations3283,126658 @node Coq Proof GeneralCoq Proof General3315,127576 @node Coq-specific commandsCoq-specific commands3331,127985 @node Coq-specific variablesCoq-specific variables3353,128492 @node Editing multiple proofsEditing multiple proofs3391,129707 @node User-loaded tacticsUser-loaded tactics3415,130815 @node Holes featureHoles feature3480,133342 @node Isabelle Proof GeneralIsabelle Proof General3507,134628 @node Classic IsabelleClassic Isabelle3576,137951 @node ML filesML files3592,138389 @node Theory filesTheory files3663,140814 @node General commands for IsabelleGeneral commands for Isabelle3717,143285 @node Specific commands for IsabelleSpecific commands for Isabelle3729,143767 @node Isabelle customizationsIsabelle customizations3758,144707 @node Isabelle/IsarIsabelle/Isar3823,146805 @node General commands for Isabelle/IsarGeneral commands for Isabelle/Isar3844,147568 @node Specific commands for Isabelle/IsarSpecific commands for Isabelle/Isar3851,147822 @node Logics and SettingsLogics and Settings3938,150350 @node HOL Proof GeneralHOL Proof General3979,152038 @node Shell Proof GeneralShell Proof General4020,153822 @node Obtaining and InstallingObtaining and Installing4056,155280 @node Obtaining Proof GeneralObtaining Proof General4072,155693 @node Installing Proof General from tarballInstalling Proof General from tarball4103,156932 @node Installing Proof General from RPM packageInstalling Proof General from RPM package4128,157764 @node Setting the names of binariesSetting the names of binaries4143,158172 @node Notes for syssiesNotes for syssies4171,159100 @node Known bugs and workaroundsKnown bugs and workarounds4244,162049 @node ReferencesReferences4257,162482 @node History of Proof GeneralHistory of Proof General4297,163506 @node Old News for 3.0Old News for 3.04388,167608 @node Old News for 3.1Old News for 3.14458,171302 @node Old News for 3.2Old News for 3.24484,172474 @node Old News for 3.3Old News for 3.34545,175477 @node Old News for 3.4Old News for 3.44564,176374 @node Function IndexFunction Index4587,177430 @node Variable IndexVariable Index4591,177506 @node Keystroke IndexKeystroke Index4595,177586 @node Concept IndexConcept Index4599,177652 doc/PG-adapting.texi,3791 @node TopTop157,4774 @node IntroductionIntroduction194,5888 @node FutureFuture235,7541 @node CreditsCredits271,9137 @node Beginning with a new proverBeginning with a new prover281,9429 @node Overview of adding a new proverOverview of adding a new prover322,11378 @node Demonstration instance and easy configurationDemonstration instance and easy configuration396,14799 @node Major modes used by Proof GeneralMajor modes used by Proof General465,18190 @node Menus and toolbar and user-level commandsMenus and toolbar and user-level commands538,21273 @node Settings for generic user-level commandsSettings for generic user-level commands553,21819 @node Menu configurationMenu configuration598,23555 @node Toolbar configurationToolbar configuration622,24473 @node Proof script settingsProof script settings680,26718 @node Recognizing commands and commentsRecognizing commands and comments702,27298 @node Recognizing proofsRecognizing proofs823,32825 @node Recognizing other elementsRecognizing other elements935,37639 @node Configuring undo behaviourConfiguring undo behaviour1061,43117 @node Nested proofsNested proofs1199,48458 @node Safe (state-preserving) commandsSafe (state-preserving) commands1239,50085 @node Activate scripting hookActivate scripting hook1262,51031 @node Automatic multiple filesAutomatic multiple files1286,51895 @node CompletionsCompletions1308,52742 @node Proof shell settingsProof shell settings1348,54218 @node Proof shell commandsProof shell commands1379,55500 @node Script input to the shellScript input to the shell1542,62375 @node Settings for matching various output from proof processSettings for matching various output from proof process1609,65418 @node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1740,71182 @node Hooks and other settingsHooks and other settings1950,80735 @node Goals buffer settingsGoals buffer settings2046,84568 @node Splash screen settingsSplash screen settings2123,87676 @node Global constantsGlobal constants2149,88434 @node Handling multiple filesHandling multiple files2175,89283 @node Configuring Font LockConfiguring Font Lock2327,97067 @node Configuring X-SymbolConfiguring X-Symbol2370,98960 @node Writing more lisp codeWriting more lisp code2430,101483 @node Default values for generic settingsDefault values for generic settings2447,102128 @node Adding prover-specific configurationsAdding prover-specific configurations2477,103211 @node Useful variablesUseful variables2520,104481 @node Useful functions and macrosUseful functions and macros2546,105275 @node Internals of Proof GeneralInternals of Proof General2648,109152 @node SpansSpans2676,110060 @node Proof General site configurationProof General site configuration2689,110434 @node Configuration variable mechanismsConfiguration variable mechanisms2769,113578 @node Global variablesGlobal variables2887,118814 @node Proof script modeProof script mode2957,121364 @node Proof shell modeProof shell mode3216,133019 @node DebuggingDebugging3622,149066 @node Plans and ideasPlans and ideas3665,149961 @node Proof by pointing and similar featuresProof by pointing and similar features3686,150683 @node Granularity of atomic command sequencesGranularity of atomic command sequences3724,152341 @node Browser mode for script files and theoriesBrowser mode for script files and theories3769,154566 @node Demonstration InstantiationsDemonstration Instantiations3799,155597 @node demoisa-easy.eldemoisa-easy.el3815,156028 @node demoisa.eldemoisa.el3878,158266 @node Function IndexFunction Index4046,163782 @node Variable IndexVariable Index4050,163858 @node Concept IndexConcept Index4059,164037