ccc/ccc.el,87
(defvar ccc-keywords 17,587
(defvar ccc-tactics 18,613
(defvar ccc-tacticals 19,638

coq/coq-abbrev.el,495
(defun holes-show-doc 12,313
(defun coq-local-vars-list-show-doc 16,390
(defconst coq-tactics-menu21,490
(defconst coq-tactics-abbrev-table26,667
(defconst coq-tacticals-menu29,784
(defconst coq-tacticals-abbrev-table33,893
(defconst coq-commands-menu36,984
(defconst coq-commands-abbrev-table43,1207
(defconst coq-terms-menu46,1296
(defconst coq-terms-abbrev-table51,1434
(defun coq-install-abbrevs 58,1628
(defpgdefault menu-entries78,2365
(defpgdefault help-menu-entries141,4384

coq/coq-db.el,668
(defconst coq-syntax-db 23,544
(defvar coq-user-tactics-db59,1917
(defun coq-insert-from-db 69,2266
(defun coq-build-regexp-list-from-db 87,2998
(defun max-length-db 109,3981
(defun coq-build-menu-from-db-internal 121,4256
(defun coq-build-title-menu 156,5879
(defun coq-sort-menu-entries 165,6247
(defun coq-build-menu-from-db 171,6374
(defcustom coq-holes-minor-mode 193,7213
(defun coq-build-abbrev-table-from-db 199,7357
(defun filter-state-preserving 218,7995
(defun filter-state-changing 223,8149
(defface coq-solve-tactics-face230,8370
(defface coq-cheat-face239,8700
(defconst coq-solve-tactics-face 247,8948
(defconst coq-cheat-face 251,9112

coq/coq.el,6010
(defcustom coq-translate-to-v8 48,1381
(defun coq-build-prog-args 54,1561
(defcustom coq-compile-file-command 64,1857
(defcustom coq-use-makefile 72,2176
(defcustom coq-default-undo-limit 80,2399
(defconst coq-shell-init-cmd85,2527
(defcustom coq-prog-env 91,2654
(defconst coq-shell-restart-cmd 99,2904
(defvar coq-shell-prompt-pattern101,2958
(defvar coq-shell-cd 109,3261
(defvar coq-shell-proof-completed-regexp 113,3421
(defvar coq-goal-regexp116,3576
(defun coq-library-directory 123,3690
(defcustom coq-tags 130,3869
(defconst coq-interrupt-regexp 135,4019
(defcustom coq-www-home-page 140,4140
(defvar coq-outline-regexp147,4308
(defvar coq-outline-heading-end-regexp 154,4520
(defvar coq-shell-outline-regexp 156,4574
(defvar coq-shell-outline-heading-end-regexp 157,4624
(defconst coq-state-preserving-tactics-regexp163,4789
(defconst coq-state-changing-commands-regexp165,4889
(defconst coq-state-preserving-commands-regexp167,4996
(defconst coq-commands-regexp169,5107
(defvar coq-retractable-instruct-regexp171,5184
(defvar coq-non-retractable-instruct-regexp173,5274
(defun coq-set-undo-limit 207,6151
(defun build-list-id-from-string 211,6281
(defun coq-last-prompt-info 223,6779
(defun coq-last-prompt-info-safe 235,7311
(defvar coq-last-but-one-statenum 241,7568
(defvar coq-last-but-one-proofnum 247,7865
(defvar coq-last-but-one-proofstack 250,7963
(defsubst coq-get-span-statenum 253,8073
(defsubst coq-get-span-proofnum 257,8188
(defsubst coq-get-span-proofstack 261,8303
(defsubst coq-set-span-statenum 265,8447
(defsubst coq-get-span-goalcmd 269,8578
(defsubst coq-set-span-goalcmd 273,8692
(defsubst coq-set-span-proofnum 277,8822
(defsubst coq-set-span-proofstack 281,8953
(defsubst proof-last-locked-span 285,9113
(defun proof-clone-buffer 291,9346
(defun proof-store-buffer-win 305,9903
(defun proof-store-response-win 311,10120
(defun proof-store-goals-win 315,10247
(defun coq-set-state-infos 327,10779
(defun count-not-intersection 365,12761
(defun coq-find-and-forget 396,14011
(defvar coq-current-goal 419,15059
(defun coq-goal-hyp 422,15124
(defun coq-state-preserving-p 435,15556
(defconst notation-print-kinds-table449,16057
(defun coq-PrintScope 453,16224
(defun coq-guess-or-ask-for-string 471,16773
(defun coq-ask-do 485,17341
(defsubst coq-put-into-brackets 494,17726
(defsubst coq-put-into-quotes 497,17787
(defun coq-SearchIsos 500,17847
(defun coq-SearchConstant 508,18088
(defun coq-Searchregexp 512,18181
(defun coq-SearchRewrite 518,18324
(defun coq-SearchAbout 522,18422
(defun coq-Print 528,18568
(defun coq-About 533,18693
(defun coq-LocateConstant 538,18813
(defun coq-LocateLibrary 543,18916
(defun coq-LocateNotation 548,19034
(defun coq-Pwd 556,19231
(defun coq-Inspect 561,19331
(defun coq-PrintSection(565,19431
(defun coq-Print-implicit 569,19524
(defun coq-Check 574,19675
(defun coq-Show 579,19783
(defun coq-Compile 593,20226
(defun coq-guess-command-line 605,20544
(defpacustom use-editing-holes 642,22097
(defun coq-mode-config 651,22400
(defun coq-shell-mode-config 743,25718
(defun coq-goals-mode-config 785,27441
(defun coq-response-config 792,27685
(defpacustom print-fully-explicit 817,28510
(defpacustom print-implicit 822,28658
(defpacustom print-coercions 827,28824
(defpacustom print-match-wildcards 832,28968
(defpacustom print-elim-types 837,29148
(defpacustom printing-depth 842,29314
(defpacustom undo-depth 847,29475
(defpacustom time-commands 852,29622
(defpacustom undo-limit 856,29732
(defpacustom auto-compile-vos 861,29834
(defun coq-maybe-compile-buffer 890,30948
(defun coq-ancestors-of 926,32476
(defun coq-all-ancestors-of 949,33440
(defun coq-process-require-command 960,33787
(defun coq-included-children 965,33914
(defun coq-process-file 986,34753
(defun coq-preprocessing 1001,35292
(defun coq-fake-constant-markup 1015,35727
(defun coq-create-span-menu 1031,36332
(defconst module-kinds-table1049,36845
(defconst modtype-kinds-table1053,36994
(defun coq-insert-section-or-module 1057,37123
(defconst reqkinds-kinds-table1078,37973
(defun coq-insert-requires 1082,38117
(defun coq-end-Section 1095,38597
(defun coq-insert-intros 1113,39175
(defun coq-insert-infoH-hook 1125,39708
(defun coq-insert-as 1130,39916
(defun coq-insert-match 1147,40609
(defun coq-insert-tactic 1176,41779
(defun coq-insert-tactical 1182,42018
(defun coq-insert-command 1188,42267
(defun coq-insert-term 1194,42511
(define-key coq-keymap 1200,42708
(define-key coq-keymap 1201,42766
(define-key coq-keymap 1202,42823
(define-key coq-keymap 1203,42892
(define-key coq-keymap 1204,42948
(define-key coq-keymap 1205,42997
(define-key coq-keymap 1206,43055
(define-key coq-keymap 1207,43115
(define-key coq-keymap 1208,43180
(define-key coq-keymap 1210,43243
(define-key coq-keymap 1211,43302
(define-key coq-keymap 1215,43427
(define-key coq-keymap 1217,43483
(define-key coq-keymap 1218,43533
(define-key coq-keymap 1219,43583
(define-key coq-keymap 1220,43639
(define-key coq-keymap 1221,43689
(define-key coq-keymap 1222,43743
(define-key coq-keymap 1223,43802
(define-key coq-goals-mode-map 1226,43863
(define-key coq-goals-mode-map 1227,43945
(define-key coq-goals-mode-map 1228,44027
(define-key coq-goals-mode-map 1229,44114
(define-key coq-goals-mode-map 1230,44196
(defvar last-coq-error-location 1239,44498
(defun coq-get-last-error-location 1247,44882
(defun coq-highlight-error 1297,47439
(defvar coq-allow-highlight-error 1328,48635
(defun coq-decide-highlight-error 1335,48961
(defun coq-highlight-error-hook 1340,49146
(defun first-word-of-buffer 1351,49539
(defun coq-show-first-goal 1359,49742
(defvar coq-modeline-string2 1376,50437
(defvar coq-modeline-string1 1377,50481
(defvar coq-modeline-string0 1378,50524
(defun coq-build-subgoals-string 1379,50569
(defun coq-update-minor-mode-alist 1384,50735
(defun is-not-split-vertic 1410,51806
(defun optim-resp-windows 1419,52246

coq/coq-indent.el,2223
(defconst coq-any-command-regexp20,368
(defconst coq-indent-inner-regexp23,459
(defconst coq-comment-start-regexp 33,813
(defconst coq-comment-end-regexp 34,856
(defconst coq-comment-start-or-end-regexp35,897
(defconst coq-indent-open-regexp37,1005
(defconst coq-indent-close-regexp42,1179
(defconst coq-indent-closepar-regexp 47,1360
(defconst coq-indent-closematch-regexp 48,1405
(defconst coq-indent-openpar-regexp 49,1476
(defconst coq-indent-openmatch-regexp 50,1520
(defconst coq-indent-any-regexp51,1600
(defconst coq-indent-kw56,1878
(defconst coq-indent-pattern-regexp 66,2332
(defun coq-indent-goal-command-p 70,2435
(defconst coq-end-command-regexp92,3486
(defun coq-search-comment-delimiter-forward 97,3638
(defun coq-search-comment-delimiter-backward 106,3968
(defun coq-skip-until-one-comment-backward 113,4242
(defun coq-skip-until-one-comment-forward 128,4949
(defun coq-looking-at-comment 139,5467
(defun coq-find-comment-start 143,5608
(defun coq-find-comment-end 154,6041
(defun coq-looking-at-syntactic-context 166,6534
(defconst coq-end-command-or-comment-regexp172,6756
(defconst coq-end-command-or-comment-start-regexp175,6865
(defun coq-find-not-in-comment-backward 179,6983
(defun coq-find-not-in-comment-forward 199,7884
(defun coq-find-command-end-backward 223,9023
(defun coq-find-command-end-forward 232,9414
(defun coq-find-command-end 241,9791
(defun coq-find-current-start 249,10123
(defun coq-find-real-start 258,10414
(defun coq-command-at-point 265,10633
(defun coq-indent-only-spaces-on-line 272,10918
(defun coq-indent-find-reg 278,11195
(defun coq-find-no-syntactic-on-line 292,11731
(defun coq-back-to-indentation-prevline 305,12204
(defun coq-find-unclosed 349,14112
(defun coq-find-at-same-level-zero 379,15408
(defun coq-find-unopened 407,16566
(defun coq-find-last-unopened 450,18000
(defun coq-end-offset 461,18397
(defun coq-indent-command-offset 486,19167
(defun coq-indent-expr-offset 533,20991
(defun coq-indent-comment-offset 649,25674
(defun coq-indent-offset 681,27123
(defun coq-indent-calculate 699,27985
(defun coq-indent-line 702,28073
(defun coq-indent-line-not-comments 712,28439
(defun coq-indent-region 722,28828

coq/coq-local-vars.el,280
(defconst coq-local-vars-doc 20,429
(defun coq-insert-coq-prog-name 78,2957
(defun coq-read-directory 89,3430
(defun coq-extract-directories-from-args 113,4533
(defun coq-ask-prog-args 128,5085
(defun coq-ask-prog-name 150,6149
(defun coq-ask-insert-coq-prog-name 168,6904

coq/coq-syntax.el,2563
(defcustom coq-prog-name 18,561
(defcustom coq-user-tactics-db 38,1343
(defcustom coq-user-commands-db 55,1856
(defcustom coq-user-tacticals-db 71,2375
(defcustom coq-user-solve-tactics-db 87,2896
(defcustom coq-user-cheat-tactics-db 103,3415
(defcustom coq-user-reserved-db 122,3961
(defvar coq-tactics-db140,4492
(defvar coq-solve-tactics-db298,12751
(defvar coq-solve-cheat-tactics-db321,13596
(defvar coq-tacticals-db333,13771
(defvar coq-decl-db357,14657
(defvar coq-defn-db380,15951
(defvar coq-goal-starters-db438,20313
(defvar coq-other-commands-db467,22070
(defvar coq-commands-db592,31283
(defvar coq-terms-db599,31503
(defun coq-count-match 663,34152
(defun coq-module-opening-p 679,34881
(defun coq-section-command-p 690,35292
(defun coq-goal-command-str-p 694,35389
(defun coq-goal-command-p 721,36491
(defvar coq-keywords-save-strict730,36774
(defvar coq-keywords-save739,36887
(defun coq-save-command-p 743,36965
(defvar coq-keywords-kill-goal752,37259
(defvar coq-keywords-state-changing-misc-commands756,37349
(defvar coq-keywords-goal759,37474
(defvar coq-keywords-decl762,37557
(defvar coq-keywords-defn765,37631
(defvar coq-keywords-state-changing-commands769,37706
(defvar coq-keywords-state-preserving-commands778,37966
(defvar coq-keywords-commands783,38182
(defvar coq-solve-tactics788,38330
(defvar coq-solve-cheat-tactics792,38451
(defvar coq-tacticals796,38596
(defvar coq-reserved802,38735
(defvar coq-state-changing-tactics813,39063
(defvar coq-state-preserving-tactics816,39172
(defvar coq-tactics820,39286
(defvar coq-retractable-instruct823,39375
(defvar coq-non-retractable-instruct826,39485
(defvar coq-keywords830,39613
(defvar coq-symbols837,39780
(defvar coq-error-regexp 856,39993
(defvar coq-id 859,40221
(defvar coq-id-shy 860,40246
(defvar coq-ids 862,40300
(defun coq-first-abstr-regexp 864,40341
(defcustom coq-variable-highlight-enable 867,40436
(defvar coq-font-lock-terms873,40563
(defconst coq-save-command-regexp-strict894,41562
(defconst coq-save-command-regexp898,41728
(defconst coq-save-with-hole-regexp903,41881
(defconst coq-goal-command-regexp907,42039
(defconst coq-goal-with-hole-regexp910,42139
(defconst coq-decl-with-hole-regexp914,42271
(defconst coq-defn-with-hole-regexp921,42519
(defconst coq-with-with-hole-regexp931,42807
(defconst coq-require-command-regexp938,43100
(defvar coq-font-lock-keywords-1946,43325
(defvar coq-font-lock-keywords 974,44727
(defun coq-init-syntax-table 976,44785
(defconst coq-generic-expression1005,45683

coq/coq-unicode-tokens.el,454
(defconst coq-token-format 39,1427
(defconst coq-token-match 40,1475
(defconst coq-hexcode-match 41,1506
(defun coq-unicode-tokens-set 43,1540
(defcustom coq-token-symbol-map49,1768
(defcustom coq-shortcut-alist152,4361
(defconst coq-control-char-format-regexp241,6379
(defconst coq-control-char-format 245,6504
(defconst coq-control-characters247,6547
(defconst coq-control-region-format-regexp 251,6639
(defconst coq-control-regions253,6722

demoisa/demoisa.el,349
(defcustom isabelledemo-prog-name 56,1848
(defcustom isabelledemo-web-page61,1970
(defun demoisa-config 72,2200
(defun demoisa-shell-config 93,2992
(define-derived-mode demoisa-mode 118,3921
(define-derived-mode demoisa-shell-mode 123,4044
(define-derived-mode demoisa-response-mode 128,4187
(define-derived-mode demoisa-goals-mode 132,4314

hol98/hol98.el,121
(defvar hol98-keywords 17,419
(defvar hol98-rules 18,447
(defvar hol98-tactics 19,472
(defvar hol98-tacticals 20,499

isar/isabelle-system.el,1254
(defgroup isabelle 28,798
(defcustom isabelle-web-page32,926
(defcustom isa-isabelle-command41,1143
(defvar isabelle-not-found 59,1825
(defun isa-set-isabelle-command 62,1940
(defun isa-shell-command-to-string 85,2958
(defun isa-getenv 91,3182
(defcustom isabelle-program-name-override 111,3881
(defun isa-tool-list-logics 122,4227
(defcustom isabelle-logics-available 129,4473
(defcustom isabelle-chosen-logic 139,4810
(defvar isabelle-chosen-logic-prev 155,5394
(defun isabelle-hack-local-variables-function 158,5514
(defun isabelle-set-prog-name 170,5953
(defun isabelle-choose-logic 194,7073
(defun isa-view-doc 213,7835
(defun isa-tool-list-docs 220,8061
(defconst isabelle-verbatim-regexp 238,8791
(defun isabelle-verbatim 241,8933
(defcustom isabelle-refresh-logics 248,9094
(defvar isabelle-docs-menu256,9422
(defvar isabelle-logics-menu-entries 263,9707
(defun isabelle-logics-menu-calculate 266,9780
(defvar isabelle-time-to-refresh-logics 287,10422
(defun isabelle-logics-menu-refresh 291,10517
(defun isabelle-menu-bar-update-logics 306,11150
(defun isabelle-load-isar-keywords 322,11779
(defun isabelle-create-span-menu 343,12507
(defun isabelle-xml-sml-escapes 359,12938
(defun isabelle-process-pgip 362,13039

isar/isar-autotest.el,31
(defvar isar-long-tests 8,187

isar/isar.el,1595
(defcustom isar-keywords-name 40,919
(defpgdefault completion-table 56,1430
(defcustom isar-web-page58,1483
(defun isar-strip-terminators 72,1833
(defun isar-markup-ml 85,2210
(defun isar-mode-config-set-variables 90,2345
(defun isar-shell-mode-config-set-variables 155,5142
(defun isar-set-proof-find-theorems-command 236,8276
(defpacustom use-find-theorems-form 242,8460
(defun isar-set-undo-commands 247,8626
(defpacustom use-linear-undo 258,9077
(defun isar-configure-from-settings 263,9235
(defun isar-remove-file 271,9379
(defun isar-shell-compute-new-files-list 283,9683
(define-derived-mode isar-shell-mode 302,10255
(define-derived-mode isar-response-mode 307,10382
(define-derived-mode isar-goals-mode 312,10515
(define-derived-mode isar-mode 317,10641
(defpgdefault menu-entries370,12358
(defun isar-set-command 401,13552
(defpgdefault help-menu-entries 406,13682
(defun isar-count-undos 409,13758
(defun isar-find-and-forget 435,14740
(defun isar-goal-command-p 471,16092
(defun isar-global-save-command-p 476,16269
(defvar isar-current-goal 497,17053
(defun isar-state-preserving-p 500,17119
(defvar isar-shell-current-line-width 525,17968
(defun isar-shell-adjust-line-width 530,18160
(defsubst isar-string-wrapping 553,18925
(defsubst isar-positions-of 562,19119
(defcustom isar-wrap-commands-singly 568,19324
(defun isar-command-wrapping 574,19520
(defun isar-preprocessing 582,19834
(defun isar-mode-config 600,20385
(defun isar-shell-mode-config 614,21038
(defun isar-response-mode-config 624,21387
(defun isar-goals-mode-config 634,21722

isar/isar-find-theorems.el,779
(defvar isar-find-theorems-data 19,565
(defun isar-find-theorems-minibuffer 35,1039
(defun isar-find-theorems-form 49,1658
(defvar isar-find-theorems-widget-number 92,3532
(defvar isar-find-theorems-widget-pattern 95,3630
(defvar isar-find-theorems-widget-intro 98,3722
(defvar isar-find-theorems-widget-elim 101,3808
(defvar isar-find-theorems-widget-dest 104,3892
(defvar isar-find-theorems-widget-name 107,3976
(defvar isar-find-theorems-widget-simp 110,4063
(defun isar-find-theorems-create-searchform115,4209
(defun isar-find-theorems-create-help 255,8752
(defun isar-find-theorems-submit-searchform298,10924
(defun isar-find-theorems-parse-criteria 376,13294
(defun isar-find-theorems-parse-number 469,16275
(defun isar-find-theorems-filter-empty 479,16552

isar/isar-keywords.el,1064
(defconst isar-keywords-major7,222
(defconst isar-keywords-minor280,4856
(defconst isar-keywords-control339,5659
(defconst isar-keywords-diag360,6153
(defconst isar-keywords-theory-begin434,7438
(defconst isar-keywords-theory-switch437,7491
(defconst isar-keywords-theory-end440,7537
(defconst isar-keywords-theory-heading443,7585
(defconst isar-keywords-theory-decl449,7692
(defconst isar-keywords-theory-script552,9481
(defconst isar-keywords-theory-goal555,9544
(defconst isar-keywords-qed583,10059
(defconst isar-keywords-qed-block590,10145
(defconst isar-keywords-qed-global593,10192
(defconst isar-keywords-proof-heading596,10241
(defconst isar-keywords-proof-goal601,10324
(defconst isar-keywords-proof-block606,10401
(defconst isar-keywords-proof-open610,10463
(defconst isar-keywords-proof-close613,10509
(defconst isar-keywords-proof-chain616,10556
(defconst isar-keywords-proof-decl623,10659
(defconst isar-keywords-proof-asm635,10821
(defconst isar-keywords-proof-asm-goal642,10916
(defconst isar-keywords-proof-script648,11005

isar/isar-mmm.el,81
(defconst isar-start-latex-regexp24,744
(defconst isar-start-sml-regexp36,1172

isar/isar-syntax.el,3975
(defconst isar-script-syntax-table-entries18,484
(defconst isar-script-syntax-table-alist42,886
(defun isar-init-syntax-table 51,1169
(defun isar-init-output-syntax-table 59,1416
(defconst isar-keyword-begin 74,1858
(defconst isar-keyword-end 75,1896
(defconst isar-keywords-theory-enclose77,1931
(defconst isar-keywords-theory82,2069
(defconst isar-keywords-save87,2200
(defconst isar-keywords-proof-enclose92,2315
(defconst isar-keywords-proof98,2476
(defconst isar-keywords-proof-context105,2653
(defconst isar-keywords-local-goal109,2760
(defconst isar-keywords-proper113,2865
(defconst isar-keywords-improper118,2984
(defconst isar-keyword-level-alist123,3116
(defconst isar-keywords-outline 138,3587
(defconst isar-keywords-indent-open141,3663
(defconst isar-keywords-indent-close147,3826
(defconst isar-keywords-indent-enclose151,3924
(defconst isar-ext-first 160,4118
(defconst isar-ext-rest 161,4185
(defconst isar-long-id-stuff 163,4257
(defconst isar-id 164,4331
(defconst isar-idx 165,4401
(defconst isar-string 167,4460
(defun isar-ids-to-regexp 169,4520
(defconst isar-any-command-regexp201,6312
(defconst isar-name-regexp208,6685
(defconst isar-improper-regexp214,6980
(defconst isar-save-command-regexp218,7128
(defconst isar-global-save-command-regexp221,7229
(defconst isar-goal-command-regexp224,7343
(defconst isar-local-goal-command-regexp227,7451
(defconst isar-comment-start 230,7564
(defconst isar-comment-end 231,7599
(defconst isar-comment-start-regexp 232,7632
(defconst isar-comment-end-regexp 233,7703
(defconst isar-string-start-regexp 235,7771
(defconst isar-string-end-regexp 236,7823
(defun isar-syntactic-context 238,7874
(defconst isar-antiq-regexp253,8269
(defconst isar-nesting-regexp259,8420
(defun isar-nesting 262,8518
(defun isar-match-nesting 274,8911
(defface isabelle-string-face 286,9245
(defface isabelle-quote-face 294,9445
(defface isabelle-class-name-face302,9641
(defface isabelle-tfree-name-face310,9828
(defface isabelle-tvar-name-face318,10021
(defface isabelle-free-name-face326,10213
(defface isabelle-bound-name-face334,10401
(defface isabelle-var-name-face342,10592
(defconst isabelle-string-face 350,10783
(defconst isabelle-quote-face 351,10837
(defconst isabelle-class-name-face 352,10890
(defconst isabelle-tfree-name-face 353,10952
(defconst isabelle-tvar-name-face 354,11014
(defconst isabelle-free-name-face 355,11075
(defconst isabelle-bound-name-face 356,11136
(defconst isabelle-var-name-face 357,11198
(defun isar-font-lock-fontify-syntactically-region 363,11347
(defvar isar-font-lock-keywords-1398,12623
(defun isar-output-flkprops 416,13631
(defun isar-output-flk 422,13883
(defvar isar-output-font-lock-keywords-1425,13992
(defun isar-strip-output-markup 461,15415
(defconst isar-shell-font-lock-keywords465,15551
(defvar isar-goals-font-lock-keywords468,15635
(defconst isar-linear-undo 502,16314
(defconst isar-undo 504,16357
(defconst isar-pr506,16400
(defun isar-remove 513,16558
(defun isar-undos 516,16633
(defun isar-cannot-undo 526,16867
(defconst isar-undo-commands529,16937
(defconst isar-theory-start-regexp537,17074
(defconst isar-end-regexp543,17232
(defconst isar-undo-fail-regexp547,17333
(defconst isar-undo-skip-regexp551,17437
(defconst isar-undo-ignore-regexp554,17558
(defconst isar-undo-remove-regexp557,17623
(defconst isar-keywords-imenu565,17780
(defconst isar-entity-regexp 572,17971
(defconst isar-named-entity-regexp575,18067
(defconst isar-named-entity-name-match-number580,18197
(defconst isar-generic-expression583,18298
(defconst isar-indent-any-regexp594,18532
(defconst isar-indent-inner-regexp596,18625
(defconst isar-indent-enclose-regexp598,18691
(defconst isar-indent-open-regexp600,18807
(defconst isar-indent-close-regexp602,18917
(defconst isar-outline-regexp608,19054
(defconst isar-outline-heading-end-regexp 612,19207
(defconst isar-outline-heading-alist 614,19256

isar/isar-unicode-tokens.el,1363
(defgroup isabelle-tokens 25,672
(defun isar-set-and-restart-tokens 30,812
(defconst isar-control-region-format-regexp43,1165
(defconst isar-control-char-format-regexp46,1259
(defconst isar-control-char-format	52,1406
(defconst isar-control-region-format-start 53,1455
(defconst isar-control-region-format-end 54,1509
(defcustom isar-control-characters57,1565
(defcustom isar-control-regions71,1978
(defconst isar-token-format 97,2790
(defconst isar-token-variant-format-regexp101,2941
(defcustom isar-greek-letters-tokens104,3055
(defcustom isar-misc-letters-tokens144,3913
(defcustom isar-symbols-tokens156,4231
(defcustom isar-extended-symbols-tokens362,9042
(defun isar-try-char 431,10697
(defcustom isar-symbols-tokens-fallbacks435,10841
(defcustom isar-bold-nums-tokens462,11771
(defun isar-map-letters 478,12160
(defconst isar-script-letters-tokens 484,12308
(defconst isar-roman-letters-tokens 489,12462
(defconst isar-fraktur-uppercase-letters-tokens 494,12636
(defconst isar-fraktur-lowercase-letters-tokens 499,12805
(defcustom isar-token-symbol-map 504,12996
(defcustom isar-user-tokens 520,13465
(defun isar-init-token-symbol-map 527,13702
(defcustom isar-symbol-shortcuts552,14351
(defcustom isar-shortcut-alist 624,16550
(defun isar-init-shortcut-alists 632,16809
(defconst isar-tokens-customizable-variables653,17472

lclam/lclam.el,524
(defcustom lclam-prog-name 18,431
(defcustom lclam-web-page24,579
(defun lclam-config 35,809
(defun lclam-shell-config 57,1600
(define-derived-mode lclam-proofscript-mode 76,2215
(define-derived-mode lclam-shell-mode 81,2338
(define-derived-mode lclam-response-mode 86,2472
(define-derived-mode lclam-goals-mode 90,2595
(defun lclam-mode 98,2823
(define-derived-mode thy-mode 135,3669
(defvar thy-mode-map 138,3767
(defun thy-add-menus 140,3794
(defun process-thy-file 179,5275
(defun update-thy-only 185,5476

lego/lego.el,1636
(defcustom lego-tags 21,535
(defcustom lego-test-all-name 26,671
(defpgdefault help-menu-entries32,829
(defpgdefault menu-entries36,989
(defvar lego-shell-handle-output47,1290
(defconst lego-process-config55,1588
(defconst lego-pretty-set-width 66,2019
(defconst lego-interrupt-regexp 70,2161
(defcustom lego-www-home-page 75,2278
(defcustom lego-www-latest-release80,2402
(defcustom lego-www-refcard86,2577
(defcustom lego-library-www-page92,2726
(defvar lego-prog-name 101,2942
(defvar lego-shell-cd 104,3011
(defvar lego-shell-proof-completed-regexp 107,3110
(defvar lego-save-command-regexp110,3250
(defvar lego-goal-command-regexp112,3340
(defvar lego-kill-goal-command 115,3431
(defvar lego-forget-id-command 116,3474
(defvar lego-undoable-commands-regexp118,3520
(defvar lego-goal-regexp 127,3894
(defvar lego-outline-regexp129,3939
(defvar lego-outline-heading-end-regexp 135,4114
(defvar lego-shell-outline-regexp 137,4167
(defvar lego-shell-outline-heading-end-regexp 138,4219
(define-derived-mode lego-shell-mode 144,4498
(define-derived-mode lego-mode 151,4659
(define-derived-mode lego-goals-mode 162,4969
(defun lego-count-undos 173,5395
(defun lego-goal-command-p 192,6148
(defun lego-find-and-forget 197,6319
(defun lego-goal-hyp 239,8155
(defun lego-state-preserving-p 248,8352
(defvar lego-shell-current-line-width 264,9055
(defun lego-shell-adjust-line-width 272,9362
(defun lego-mode-config 289,10063
(defun lego-equal-module-filename 357,12112
(defun lego-shell-compute-new-files-list 363,12387
(defun lego-shell-mode-config 373,12770
(defun lego-goals-mode-config 420,14437

lego/lego-syntax.el,600
(defconst lego-keywords-goal 15,358
(defconst lego-keywords-save 17,401
(defconst lego-commands19,472
(defconst lego-keywords31,1030
(defconst lego-tacticals 36,1207
(defconst lego-error-regexp 39,1315
(defvar lego-id 42,1473
(defvar lego-ids 44,1500
(defconst lego-arg-list-regexp 48,1696
(defun lego-decl-defn-regexp 51,1812
(defconst lego-definiendum-alternative-regexp59,2184
(defvar lego-font-lock-terms63,2368
(defconst lego-goal-with-hole-regexp89,3221
(defconst lego-save-with-hole-regexp94,3443
(defvar lego-font-lock-keywords-199,3660
(defun lego-init-syntax-table 110,4122

phox/phox.el,555
(defcustom phox-prog-name 32,916
(defcustom phox-web-page37,1018
(defcustom phox-doc-dir43,1168
(defcustom phox-lib-dir49,1315
(defcustom phox-tags-program55,1458
(defcustom phox-tags-doc61,1637
(defcustom phox-etags67,1774
(defpgdefault menu-entries88,2224
(defun phox-config 102,2417
(defun phox-shell-config 146,4341
(define-derived-mode phox-mode 170,5203
(define-derived-mode phox-shell-mode 186,5666
(define-derived-mode phox-response-mode 191,5794
(define-derived-mode phox-goals-mode 201,6155
(defpgdefault completion-table224,6941

phox/phox-extraction.el,383
(defvar phox-prog-orig 19,619
(defun phox-prog-flags-modify(21,687
(defun phox-prog-flags-extract(50,1488
(defun phox-prog-flags-erase(61,1778
(defun phox-toggle-extraction(69,1974
(defun phox-compile-theorem(81,2376
(defun phox-compile-theorem-on-cursor(87,2601
(defun phox-output 103,3079
(defun phox-output-theorem 113,3291
(defun phox-output-theorem-on-cursor(120,3590

phox/phox-font.el,231
(defvar phox-sym-lock-enabled 1,0
(defvar phox-sym-lock-color 2,60
(defvar phox-sym-lock-keywords 3,118
(defconst phox-font-lock-keywords11,511
(defconst phox-sym-lock-keywords-table70,2628
(defun phox-sym-lock-start 93,3202

phox/phox-fun.el,1659
(defconst phox-forget-id-command 11,186
(defconst phox-forget-proof-command 12,232
(defconst phox-forget-new-elim-command 13,287
(defconst phox-forget-new-intro-command 14,345
(defconst phox-forget-new-equation-command 15,405
(defconst phox-forget-close-def-command 16,471
(defconst phox-comments-regexp 18,597
(defconst phox-strict-comments-regexp 20,776
(defconst phox-ident-regexp 21,941
(defconst phox-inductive-option 22,1027
(defconst phox-spaces-regexp 23,1079
(defconst phox-sy-definition-regexp 24,1122
(defconst phox-sy-inductive-regexp 28,1309
(defconst phox-inductive-regexp 34,1522
(defconst phox-data-regexp 40,1673
(defconst phox-definition-regexp 46,1827
(defconst phox-prove-claim-regexp 50,1971
(defconst phox-new-elim-regexp 54,2077
(defconst phox-new-intro-regexp 57,2196
(defconst phox-new-rewrite-regexp 60,2317
(defconst phox-new-equation-regexp 63,2442
(defconst phox-close-def-regexp 66,2569
(defun phox-init-syntax-table 71,2706
(defvar phox-top-keywords87,3178
(defvar phox-proof-keywords135,3633
(defun phox-find-and-forget 176,3983
(defalias 'phox-assert-next-command-interactive phox-assert-next-command-interactive
255,6399
(defun phox-depend-theorem(274,7365
(defun phox-eshow-extlist(283,7654
(defun phox-flag-name(297,8251
(defun phox-path(308,8553
(defun phox-print-expression(319,8789
(defun phox-print-sort-expression(332,9245
(defun phox-priority-symbols-list(343,9557
(defun phox-search-string(355,9929
(defun phox-constraints(370,10454
(defun phox-goals(381,10710
(defvar phox-state-menu393,10919
(defun phox-delete-symbol(418,11909
(defun phox-delete-symbol-on-cursor(424,12117

phox/phox-lang.el,323
(defvar phox-lang9,306
(defun phox-lang-absurd 17,535
(defun phox-lang-suppress 22,629
(defun phox-lang-opendef 27,826
(defun phox-lang-instance 32,944
(defun phox-lang-open-instance 37,1073
(defun phox-lang-lock 42,1222
(defun phox-lang-unlock 47,1352
(defun phox-lang-prove 52,1488
(defun phox-lang-let 57,1622

phox/phox-outline.el,254
(defconst phox-outline-title-regexp 20,745
(defconst phox-outline-section-regexp 21,810
(defconst phox-outline-save-regexp 22,866
(defconst phox-outline-heading-end-regexp 39,1409
(defun phox-outline-level(45,1584
(defun phox-setup-outline 59,2058

phox/phox-pbrpm.el,513
(defun phox-pbrpm-left-paren-p 39,1671
(defun phox-pbrpm-right-paren-p 46,1874
(defun phox-pbrpm-menu-from-string 54,2078
(defun phox-pbrpm-rename-in-cmd 63,2410
(defun phox-pbrpm-get-region-name 96,3658
(defun  phox-pbrpm-escape-string 99,3785
(defun phox-pbrpm-generate-menu 103,3920
(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu
310,11400
(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p
311,11464
(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
312,11526

phox/phox-sym-lock.el,1398
(defcustom phox-sym-lock-enabled 19,871
(defvar phox-sym-lock-sym-count 59,2452
(defvar phox-sym-lock-ext-start 62,2522
(defvar phox-sym-lock-ext-end 64,2644
(defvar phox-sym-lock-font-size 67,2763
(defvar phox-sym-lock-keywords 72,2953
(defvar phox-sym-lock-enabled 77,3129
(defvar phox-sym-lock-color 82,3291
(defvar phox-sym-lock-mouse-face 87,3509
(defvar phox-sym-lock-mouse-face-enabled 92,3699
(defconst phox-sym-lock-with-mule 97,3889
(defun phox-sym-lock-gen-symbol 100,3973
(defun phox-sym-lock-make-symbols-atomic 108,4275
(defun phox-sym-lock-compute-font-size 135,5216
(defvar phox-sym-lock-font-name173,6635
(defun phox-sym-lock-set-foreground 216,8233
(defun phox-sym-lock-translate-char 230,8842
(defun phox-sym-lock-translate-char-or-string 239,9159
(defun phox-sym-lock-remap-face 246,9387
(defvar phox-sym-lock-clear-face266,10375
(defun phox-sym-lock 278,10794
(defun phox-sym-lock-rec 287,11198
(defun phox-sym-lock-atom-face 293,11343
(defun phox-sym-lock-pre-idle-hook-first 298,11639
(defun phox-sym-lock-pre-idle-hook-last 308,12044
(defun phox-sym-lock-enable 317,12419
(defun phox-sym-lock-disable 330,12830
(defun phox-sym-lock-mouse-face-enable 343,13246
(defun phox-sym-lock-mouse-face-disable 350,13461
(defun phox-sym-lock-font-lock-hook 357,13680
(defun font-lock-set-defaults 372,14371
(defun phox-sym-lock-patch-keywords 384,14798

phox/phox-tags.el,305
(defun phox-tags-add-table(26,869
(defun phox-tags-reset-table(35,1264
(defun phox-tags-add-doc-table(40,1374
(defun phox-tags-add-lib-table(46,1523
(defun phox-tags-add-local-table(52,1658
(defun phox-tags-create-local-table(58,1841
(defun phox-complete-tag(69,2091
(defvar phox-tags-menu76,2200

plastic/plastic.el,2759
(defcustom plastic-tags 29,608
(defcustom plastic-test-all-name 34,740
(defvar plastic-lit-string41,931
(defcustom plastic-help-menu-list45,1043
(defvar plastic-shell-handle-output59,1536
(defconst plastic-process-config67,1837
(defconst plastic-pretty-set-width 74,2085
(defconst plastic-interrupt-regexp 78,2233
(defcustom plastic-www-home-page 84,2354
(defcustom plastic-www-latest-release89,2491
(defcustom plastic-www-refcard95,2661
(defcustom plastic-library-www-page101,2792
(defcustom plastic-base111,3007
(defvar plastic-prog-name119,3178
(defun plastic-set-default-env-vars 123,3285
(defvar plastic-shell-cd131,3522
(defvar plastic-shell-proof-completed-regexp 135,3662
(defvar plastic-save-command-regexp138,3805
(defvar plastic-goal-command-regexp140,3901
(defvar plastic-kill-goal-command143,3998
(defvar plastic-forget-id-command145,4098
(defvar plastic-undoable-commands-regexp148,4178
(defvar plastic-goal-regexp 160,4625
(defvar plastic-outline-regexp162,4673
(defvar plastic-outline-heading-end-regexp 168,4851
(defvar plastic-shell-outline-regexp 170,4907
(defvar plastic-shell-outline-heading-end-regexp 171,4965
(defvar plastic-error-occurred173,5036
(define-derived-mode plastic-shell-mode 182,5353
(define-derived-mode plastic-mode 188,5535
(define-derived-mode plastic-goals-mode 204,6052
(defun plastic-count-undos 213,6397
(defun plastic-goal-command-p 234,7284
(defun plastic-find-and-forget 239,7476
(defun plastic-goal-hyp 278,8887
(defun plastic-state-preserving-p 289,9136
(defvar plastic-shell-current-line-width 312,10111
(defun plastic-shell-adjust-line-width 320,10427
(defun plastic-mode-config 345,11436
(defun plastic-show-shell-buffer 434,14695
(defun plastic-equal-module-filename 440,14798
(defun plastic-shell-compute-new-files-list 446,15076
(defun plastic-shell-mode-config 458,15470
(defun plastic-goals-mode-config 506,17273
(defun plastic-small-bar 518,17560
(defun plastic-large-bar 520,17649
(defun plastic-preprocessing 522,17787
(defun plastic-all-ctxt 574,19590
(defun plastic-send-one-undo 581,19759
(defun plastic-minibuf-cmd 591,20065
(defun plastic-minibuf 603,20537
(defun plastic-synchro 610,20743
(defun plastic-send-minibuf 615,20884
(defun plastic-had-error 623,21192
(defun plastic-reset-error 627,21367
(defun plastic-call-if-no-error 630,21506
(defun plastic-show-shell 635,21710
(define-key plastic-keymap 640,21838
(define-key plastic-keymap 641,21899
(define-key plastic-keymap 642,21960
(define-key plastic-keymap 643,22020
(define-key plastic-keymap 644,22079
(define-key plastic-keymap 645,22138
(defalias 'proof-toolbar-command proof-toolbar-command
655,22387
(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
656,22438

plastic/plastic-syntax.el,648
(defconst plastic-keywords-goal 18,536
(defconst plastic-keywords-save 20,582
(defconst plastic-commands22,656
(defconst plastic-keywords35,1263
(defconst plastic-tacticals 40,1446
(defconst plastic-error-regexp 43,1557
(defvar plastic-id 46,1690
(defvar plastic-ids 48,1720
(defconst plastic-arg-list-regexp 52,1928
(defun plastic-decl-defn-regexp 55,2047
(defconst plastic-definiendum-alternative-regexp63,2428
(defvar plastic-font-lock-terms67,2621
(defconst plastic-goal-with-hole-regexp89,3331
(defconst plastic-save-with-hole-regexp94,3557
(defvar plastic-font-lock-keywords-199,3783
(defun plastic-init-syntax-table 108,4175

generic/pg-assoc.el,81
(defun proof-associated-buffers 33,973
(defun proof-associated-windows 43,1183

generic/pg-autotest.el,868
(defvar pg-autotest-success 30,692
(defvar pg-autotest-log 33,779
(defadvice proof-debug 38,916
(defun pg-autotest-find-file 44,1092
(defun pg-autotest-find-file-restart 51,1358
(defmacro pg-autotest 64,1811
(defun pg-autotest-log 91,2532
(defun pg-autotest-message 99,2756
(defun pg-autotest-remark 108,3040
(defun pg-autotest-timestart 111,3121
(defun pg-autotest-timetaken 116,3304
(defun pg-autotest-exit 127,3668
(defun pg-autotest-test-process-wholefile 138,4019
(defun pg-autotest-test-script-wholefile 146,4306
(defun pg-autotest-test-script-randomjumps 171,5238
(defun pg-autotest-test-retract-file 221,6847
(defun pg-autotest-test-assert-processed 227,6988
(defun pg-autotest-test-assert-full 233,7214
(defun pg-autotest-test-assert-unprocessed 240,7455
(defun pg-autotest-test-eval 247,7720
(defun pg-autotest-test-quit-prover 251,7819

generic/pg-custom.el,554
(defpgcustom maths-menu-enable 36,1134
(defpgcustom unicode-tokens-enable 42,1314
(defpgcustom mmm-enable 48,1491
(defpgcustom script-indent 57,1845
(defconst proof-toolbar-entries-default62,1982
(defpgcustom toolbar-entries 90,3711
(defpgcustom prog-args 109,4444
(defpgcustom prog-env 122,5019
(defpgcustom favourites 131,5446
(defpgcustom menu-entries 136,5635
(defpgcustom help-menu-entries 143,5871
(defpgcustom keymap 150,6134
(defpgcustom completion-table 155,6305
(defpgcustom tags-program 166,6679
(defpgcustom use-holes 175,7063

generic/pg-goals.el,285
(define-derived-mode proof-goals-mode 29,734
(define-key proof-goals-mode-map 57,1609
(define-key proof-goals-mode-map 59,1725
(define-key proof-goals-mode-map 60,1793
(defun proof-goals-config-done 69,1938
(defun pg-goals-display 77,2204
(defun pg-goals-button-action 118,3508

generic/pg-movie.el,334
(defconst pg-movie-xml-header 33,944
(defconst pg-movie-stylesheet35,1002
(defun pg-movie-stylesheet-location 38,1101
(defvar pg-movie-frame 42,1209
(defun pg-movie-of-span 44,1263
(defun pg-movie-of-region 80,2383
(defun pg-movie-export 87,2571
(defun pg-movie-export-from 109,3175
(defun pg-movie-export-directory 120,3496

generic/pg-pamacs.el,486
(defmacro deflocal 37,1200
(deflocal proof-buffer-type 44,1438
(defmacro proof-ass-sym 52,1574
(defmacro proof-ass-symv 58,1833
(defmacro proof-ass 64,2091
(defun proof-defpgcustom-fn 70,2343
(defun undefpgcustom 91,3213
(defmacro defpgcustom 97,3437
(defun proof-defpgdefault-fn 108,3848
(defmacro defpgdefault 122,4306
(defmacro defpgfun 133,4668
(defun proof-defpacustom-fn 147,5067
(defmacro defpacustom 211,7251
(defmacro proof-eval-when-ready-for-assistant 232,8198

generic/pg-pbrpm.el,1808
(defvar pg-pbrpm-use-buffer-menu 45,1208
(defvar pg-pbrpm-start-goal-regexp 48,1330
(defvar pg-pbrpm-start-goal-regexp-par-num 52,1487
(defvar pg-pbrpm-end-goal-regexp 55,1610
(defvar pg-pbrpm-start-hyp-regexp 59,1762
(defvar pg-pbrpm-start-hyp-regexp-par-num 63,1923
(defvar pg-pbrpm-start-concl-regexp 67,2130
(defvar pg-pbrpm-auto-select-regexp 71,2294
(defvar pg-pbrpm-buffer-menu 78,2455
(defvar pg-pbrpm-spans 79,2489
(defvar pg-pbrpm-goal-description 80,2517
(defvar pg-pbrpm-windows-dialog-bug 81,2556
(defvar pbrpm-menu-desc 82,2597
(defun pg-pbrpm-erase-buffer-menu 84,2627
(defun pg-pbrpm-menu-change-hook 90,2799
(defun pg-pbrpm-create-reset-buffer-menu 108,3374
(defun pg-pbrpm-analyse-goal-buffer 127,4216
(defun pg-pbrpm-button-action 187,6621
(defun pg-pbrpm-exists 194,6847
(defun pg-pbrpm-eliminate-id 198,6959
(defun pg-pbrpm-build-menu 206,7205
(defun pg-pbrpm-setup-span 269,9525
(defun pg-pbrpm-run-command 329,11840
(defun pg-pbrpm-get-pos-info 362,13361
(defun pg-pbrpm-get-region-info 404,14660
(defun pg-pbrpm-auto-select-around-point 415,15072
(defun pg-pbrpm-translate-position 430,15596
(defun pg-pbrpm-process-click 438,15850
(defvar pg-pbrpm-remember-region-selected-region 458,16875
(defvar pg-pbrpm-regions-list 459,16929
(defun pg-pbrpm-erase-regions-list 461,16965
(defun pg-pbrpm-filter-regions-list 470,17273
(defface pg-pbrpm-multiple-selection-face477,17536
(defface pg-pbrpm-menu-input-face485,17738
(defun pg-pbrpm-do-remember-region 493,17928
(defun pg-pbrpm-remember-region-drag-up-hook 514,18776
(defun pg-pbrpm-remember-region-click-hook 518,18947
(defun pg-pbrpm-remember-region 523,19132
(defun pg-pbrpm-process-region 537,19846
(defun pg-pbrpm-process-regions-list 555,20575
(defun pg-pbrpm-region-expression 559,20758

generic/pg-pgip.el,2931
(defalias 'pg-pgip-debug pg-pgip-debug
38,1032
(defalias 'pg-pgip-error pg-pgip-error
39,1073
(defalias 'pg-pgip-warning pg-pgip-warning
40,1108
(defconst pg-pgip-version-supported 42,1158
(defun pg-pgip-process-packet 46,1264
(defvar pg-pgip-last-seen-id 56,1832
(defvar pg-pgip-last-seen-seq 57,1866
(defun pg-pgip-process-pgip 59,1902
(defun pg-pgip-process-msg 78,2842
(defvar pg-pgip-post-process-functions93,3433
(defun pg-pgip-post-process 103,3908
(defun pg-pgip-process-askpgip 120,4523
(defun pg-pgip-process-usespgip 126,4727
(defun pg-pgip-process-usespgml 130,4891
(defun pg-pgip-process-pgmlconfig 134,5055
(defun pg-pgip-process-proverinfo 150,5672
(defun pg-pgip-process-hasprefs 167,6337
(defun pg-pgip-haspref 181,6969
(defun pg-pgip-process-prefval 198,7671
(defun pg-pgip-process-guiconfig 225,8379
(defvar proof-assistant-idtables 232,8496
(defun pg-pgip-process-ids 235,8613
(defun pg-complete-idtable-symbol 261,9685
(defalias 'pg-pgip-process-setids pg-pgip-process-setids
266,9777
(defalias 'pg-pgip-process-addids pg-pgip-process-addids
267,9833
(defalias 'pg-pgip-process-delids pg-pgip-process-delids
268,9889
(defun pg-pgip-process-idvalue 271,9947
(defun pg-pgip-process-menuadd 283,10293
(defun pg-pgip-process-menudel 286,10336
(defun pg-pgip-process-ready 295,10568
(defun pg-pgip-process-cleardisplay 298,10609
(defun pg-pgip-process-proofstate 312,11066
(defun pg-pgip-process-normalresponse 316,11143
(defun pg-pgip-process-errorresponse 320,11273
(defun pg-pgip-process-scriptinsert 324,11402
(defun pg-pgip-process-metainforesponse 329,11536
(defun pg-pgip-file-of-url 338,11776
(defun pg-pgip-process-informfileloaded 343,11911
(defun pg-pgip-process-informfileretracted 349,12143
(defun pg-pgip-process-brokerstatus 362,12590
(defun pg-pgip-process-proveravailmsg 365,12638
(defun pg-pgip-process-newprovermsg 368,12688
(defun pg-pgip-process-proverstatusmsg 371,12736
(defvar pg-pgip-srcids 380,12982
(defun pg-pgip-process-newfile 384,13089
(defun pg-pgip-process-filestatus 400,13671
(defun pg-pgip-process-newobj 420,14325
(defun pg-pgip-process-delobj 423,14367
(defun pg-pgip-process-objectstatus 426,14409
(defun pg-pgip-process-parsescript 440,14761
(defun pg-pgip-get-pgiptype 463,15635
(defun pg-pgip-default-for 483,16427
(defun pg-pgip-subst-for 496,16822
(defun pg-pgip-interpret-value 508,17165
(defun pg-pgip-interpret-choice 526,17846
(defun pg-pgip-string-of-command 557,18863
(defconst pg-pgip-id574,19624
(defvar pg-pgip-refseq 580,19904
(defvar pg-pgip-refid 582,20001
(defvar pg-pgip-seq 585,20093
(defun pg-pgip-assemble-packet 587,20157
(defun pg-pgip-issue 605,20968
(defun pg-pgip-maybe-askpgip 622,21580
(defun pg-pgip-askprefs 628,21771
(defun pg-pgip-askids 632,21885
(defun pg-pgip-reset 645,22173
(defconst pg-pgip-start-element-regexp 676,22871
(defconst pg-pgip-end-element-regexp 677,22923

generic/pg-response.el,1292
(deflocal pg-response-eagerly-raise 32,789
(define-derived-mode proof-response-mode 42,1014
(define-key proof-response-mode-map 70,1968
(define-key proof-response-mode-map 71,2039
(define-key proof-response-mode-map 72,2093
(defun proof-response-config-done 76,2179
(defvar pg-response-special-display-regexp 87,2525
(defconst proof-multiframe-parameters91,2692
(defun proof-multiple-frames-enable 100,2982
(defun proof-three-window-enable 110,3310
(defun proof-select-three-b 113,3373
(defun proof-display-three-b 128,3842
(defvar pg-frame-configuration 139,4232
(defun pg-cache-frame-configuration 143,4379
(defun proof-layout-windows 147,4550
(defun proof-delete-other-frames 187,6337
(defvar pg-response-erase-flag 218,7425
(defun pg-response-maybe-erase222,7554
(defun pg-response-display 252,8658
(defun pg-response-display-with-face 277,9441
(defun pg-response-clear-displays 305,10287
(defun pg-response-message 318,10806
(defun pg-response-warning 324,11041
(defun proof-next-error 339,11447
(defun pg-response-has-error-location 417,14256
(defvar proof-trace-last-fontify-pos 439,15069
(defun proof-trace-fontify-pos 441,15112
(defun proof-trace-buffer-display 449,15425
(defun proof-trace-buffer-finish 460,15769
(defun pg-thms-buffer-clear 478,16112

generic/pg-user.el,3657
(defun proof-script-new-command-advance 42,1232
(defun proof-maybe-follow-locked-end 85,2994
(defun proof-goto-command-start 112,3870
(defun proof-goto-command-end 135,4817
(defun proof-goto-point 158,5342
(defun proof-assert-next-command-interactive 172,5776
(defun proof-assert-until-point-interactive 184,6262
(defun proof-process-buffer 190,6492
(defun proof-undo-last-successful-command 208,7004
(defun proof-undo-and-delete-last-successful-command 213,7166
(defun proof-undo-last-successful-command-1 226,7720
(defun proof-retract-buffer 243,8339
(defun proof-retract-current-goal 252,8623
(defun proof-mouse-goto-point 271,9143
(defvar proof-minibuffer-history 286,9419
(defun proof-minibuffer-cmd 289,9514
(defun proof-frob-locked-end 333,11136
(defmacro proof-if-setting-configured 394,13074
(defmacro proof-define-assistant-command 402,13343
(defmacro proof-define-assistant-command-witharg 415,13798
(defun proof-issue-new-command 435,14620
(defun proof-cd-sync 475,15843
(defun proof-electric-terminator-enable 531,17617
(defun proof-electric-terminator 538,17861
(defun proof-add-completions 564,18684
(defun proof-script-complete 589,19573
(defun pg-copy-span-contents 603,19882
(defun pg-numth-span-higher-or-lower 620,20440
(defun pg-control-span-of 646,21186
(defun pg-move-span-contents 652,21390
(defun pg-fixup-children-spans 704,23566
(defun pg-move-region-down 714,23823
(defun pg-move-region-up 723,24116
(defun proof-forward-command 753,24944
(defun proof-backward-command 774,25665
(defun pg-pos-for-event 796,26009
(defun pg-span-for-event 802,26230
(defun pg-span-context-menu 806,26374
(defun pg-toggle-visibility 821,26822
(defun pg-create-in-span-context-menu 830,27129
(defun pg-span-undo 859,28343
(defun pg-goals-buffers-hint 905,29745
(defun pg-slow-fontify-tracing-hint 909,29927
(defun pg-response-buffers-hint 913,30098
(defun pg-jump-to-end-hint 925,30513
(defun pg-processing-complete-hint 929,30642
(defun pg-next-error-hint 946,31362
(defun pg-hint 951,31514
(defun pg-identifier-under-mouse-query 967,32104
(defun pg-identifier-near-point-query 977,32413
(defvar proof-query-identifier-collection 1005,33310
(defvar proof-query-identifier-history 1006,33357
(defun proof-query-identifier 1008,33402
(defun pg-identifier-query 1019,33721
(defun proof-imenu-enable 1052,34887
(defvar pg-input-ring 1088,36209
(defvar pg-input-ring-index 1091,36266
(defvar pg-stored-incomplete-input 1094,36338
(defun pg-previous-input 1097,36441
(defun pg-next-input 1111,36898
(defun pg-delete-input 1116,37020
(defun pg-get-old-input 1129,37358
(defun pg-restore-input 1143,37749
(defun pg-search-start 1154,38039
(defun pg-regexp-arg 1166,38531
(defun pg-search-arg 1178,38979
(defun pg-previous-matching-input-string-position 1192,39396
(defun pg-previous-matching-input 1219,40561
(defun pg-next-matching-input 1238,41411
(defvar pg-matching-input-from-input-string 1246,41794
(defun pg-previous-matching-input-from-input 1250,41908
(defun pg-next-matching-input-from-input 1268,42673
(defun pg-add-to-input-history 1279,43052
(defun pg-remove-from-input-history 1291,43505
(defun  pg-clear-input-ring 1302,43885
(define-key proof-mode-map 1319,44355
(define-key proof-mode-map 1320,44415
(defun pg-protected-undo 1322,44487
(defun pg-protected-undo-1 1357,45877
(defun next-undo-elt 1388,47311
(defvar proof-autosend-timer 1415,48267
(deflocal proof-autosend-error-point 1417,48328
(defun proof-autosend-enable 1421,48452
(defun proof-autosend-delay 1435,48993
(defun proof-autosend-loop 1439,49126
(defun proof-autosend-loop-all 1445,49311

generic/pg-vars.el,1491
(defvar proof-assistant-cusgrp 22,389
(defvar proof-assistant-internals-cusgrp 28,649
(defvar proof-assistant 34,919
(defvar proof-assistant-symbol 39,1142
(defvar proof-mode-for-shell 52,1684
(defvar proof-mode-for-response 57,1874
(defvar proof-mode-for-goals 62,2100
(defvar proof-mode-for-script 67,2289
(defvar proof-ready-for-assistant-hook 72,2466
(defvar proof-shell-busy 83,2754
(defvar proof-shell-last-queuemode 101,3425
(defvar proof-included-files-list 105,3580
(defvar proof-script-buffer 127,4599
(defvar proof-previous-script-buffer 130,4691
(defvar proof-shell-buffer 134,4864
(defvar proof-goals-buffer 137,4950
(defvar proof-response-buffer 140,5005
(defvar proof-trace-buffer 143,5066
(defvar proof-thms-buffer 147,5220
(defvar proof-shell-error-or-interrupt-seen 151,5375
(defvar pg-response-next-error 156,5599
(defvar proof-shell-proof-completed 159,5706
(defvar proof-terminal-string 171,6250
(defvar proof-shell-silent 183,6508
(defvar proof-shell-last-prompt 186,6596
(defvar proof-shell-last-output 190,6766
(defvar proof-shell-last-output-kind 194,6906
(defvar proof-assistant-settings 214,7670
(defvar pg-tracing-slow-mode 222,8118
(defvar proof-nesting-depth 225,8207
(defvar proof-last-theorem-dependencies 232,8442
(defvar proof-autosend-running 236,8604
(defcustom proof-general-name 246,8877
(defcustom proof-general-home-page251,9034
(defcustom proof-unnamed-theorem-name257,9194
(defcustom proof-universal-keys263,9378

generic/pg-xml.el,1177
(defalias 'pg-xml-error pg-xml-error
18,381
(defun pg-xml-parse-string 41,1023
(defun pg-xml-parse-buffer 51,1335
(defun pg-xml-get-attr 70,1950
(defun pg-xml-child-elts 78,2252
(defun pg-xml-child-elt 83,2457
(defun pg-xml-get-child 91,2739
(defun pg-xml-get-text-content 101,3106
(defmacro pg-xml-attr 112,3456
(defmacro pg-xml-node 114,3518
(defconst pg-xml-header117,3610
(defun pg-xml-string-of 121,3686
(defun pg-xml-output-internal 132,4053
(defun pg-xml-cdata 166,5192
(defsubst pg-pgip-get-area 174,5385
(defun pg-pgip-get-icon 177,5502
(defsubst pg-pgip-get-name 181,5650
(defsubst pg-pgip-get-version 184,5767
(defsubst pg-pgip-get-descr 187,5890
(defsubst pg-pgip-get-thmname 190,6009
(defsubst pg-pgip-get-thyname 193,6132
(defsubst pg-pgip-get-url 196,6255
(defsubst pg-pgip-get-srcid 199,6370
(defsubst pg-pgip-get-proverid 202,6489
(defsubst pg-pgip-get-symname 205,6614
(defsubst pg-pgip-get-prefcat 208,6734
(defsubst pg-pgip-get-default 211,6862
(defsubst pg-pgip-get-objtype 214,6985
(defsubst pg-pgip-get-value 217,7108
(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
220,7178
(defun pg-pgip-get-pgmltext 222,7237

generic/proof-autoloads.el,97
(defsubst proof-shell-live-buffer 677,21893
(defsubst proof-replace-regexp-in-string 822,27138

generic/proof-auxmodes.el,149
(defun proof-mmm-support-available 20,489
(defun proof-maths-menu-support-available 44,1100
(defun proof-unicode-tokens-support-available 58,1517

generic/proof-config.el,7742
(defgroup prover-config 80,2633
(defcustom proof-guess-command-line 98,3483
(defcustom proof-assistant-home-page 113,3978
(defcustom proof-context-command 119,4148
(defcustom proof-info-command 124,4282
(defcustom proof-showproof-command 131,4553
(defcustom proof-goal-command 136,4689
(defcustom proof-save-command 144,4986
(defcustom proof-find-theorems-command 152,5295
(defcustom proof-query-identifier-command 159,5603
(defcustom proof-assistant-true-value 173,6292
(defcustom proof-assistant-false-value 179,6482
(defcustom proof-assistant-format-int-fn 185,6676
(defcustom proof-assistant-format-string-fn 192,6925
(defcustom proof-assistant-setting-format 199,7192
(defgroup proof-script 221,7887
(defcustom proof-terminal-char 226,8017
(defcustom proof-electric-terminator-noterminator 236,8404
(defcustom proof-script-sexp-commands 241,8576
(defcustom proof-script-command-end-regexp 252,9033
(defcustom proof-script-command-start-regexp 270,9852
(defcustom proof-script-integral-proofs 281,10313
(defcustom proof-script-fly-past-comments 296,10969
(defcustom proof-script-parse-function 301,11140
(defcustom proof-script-comment-start 319,11783
(defcustom proof-script-comment-start-regexp 330,12220
(defcustom proof-script-comment-end 338,12539
(defcustom proof-script-comment-end-regexp 350,12961
(defcustom proof-string-start-regexp 358,13274
(defcustom proof-string-end-regexp 363,13439
(defcustom proof-case-fold-search 368,13600
(defcustom proof-save-command-regexp 377,14012
(defcustom proof-save-with-hole-regexp 382,14122
(defcustom proof-save-with-hole-result 393,14497
(defcustom proof-goal-command-regexp 403,14937
(defcustom proof-goal-with-hole-regexp 411,15224
(defcustom proof-goal-with-hole-result 423,15667
(defcustom proof-non-undoables-regexp 432,16041
(defcustom proof-nested-undo-regexp 443,16496
(defcustom proof-ignore-for-undo-count 459,17208
(defcustom proof-script-imenu-generic-expression 467,17511
(defcustom proof-goal-command-p 475,17850
(defcustom proof-really-save-command-p 486,18341
(defcustom proof-completed-proof-behaviour 495,18648
(defcustom proof-count-undos-fn 523,19997
(defcustom proof-find-and-forget-fn 535,20548
(defcustom proof-forget-id-command 552,21257
(defcustom pg-topterm-goalhyplit-fn 562,21615
(defcustom proof-kill-goal-command 574,22150
(defcustom proof-undo-n-times-cmd 588,22654
(defcustom proof-nested-goals-history-p 602,23191
(defcustom proof-arbitrary-undo-positions 611,23528
(defcustom proof-state-preserving-p 625,24109
(defcustom proof-activate-scripting-hook 635,24581
(defcustom proof-deactivate-scripting-hook 654,25362
(defcustom proof-script-evaluate-elisp-comment-regexp 663,25692
(defcustom proof-indent 681,26278
(defcustom proof-indent-hang 686,26385
(defcustom proof-indent-enclose-offset 691,26511
(defcustom proof-indent-open-offset 696,26653
(defcustom proof-indent-close-offset 701,26790
(defcustom proof-indent-any-regexp 706,26928
(defcustom proof-indent-inner-regexp 711,27088
(defcustom proof-indent-enclose-regexp 716,27242
(defcustom proof-indent-open-regexp 721,27396
(defcustom proof-indent-close-regexp 726,27548
(defcustom proof-script-font-lock-keywords 732,27702
(defcustom proof-script-syntax-table-entries 740,28054
(defcustom proof-script-span-context-menu-extensions 758,28450
(defgroup proof-shell 784,29210
(defcustom proof-prog-name 794,29380
(defcustom proof-shell-auto-terminate-commands 805,29800
(defcustom proof-shell-pre-sync-init-cmd 814,30201
(defcustom proof-shell-init-cmd 828,30759
(defcustom proof-shell-init-hook 840,31288
(defcustom proof-shell-restart-cmd 845,31427
(defcustom proof-shell-quit-cmd 850,31582
(defcustom proof-shell-quit-timeout 855,31749
(defcustom proof-shell-cd-cmd 864,32140
(defcustom proof-shell-start-silent-cmd 881,32811
(defcustom proof-shell-stop-silent-cmd 890,33187
(defcustom proof-shell-silent-threshold 899,33522
(defcustom  proof-shell-inform-file-processed-cmd 907,33856
(defcustom  proof-shell-inform-file-retracted-cmd 928,34784
(defcustom proof-auto-multiple-files 956,36056
(defcustom proof-cannot-reopen-processed-files 971,36777
(defcustom proof-shell-require-command-regexp 985,37443
(defcustom proof-done-advancing-require-function 996,37905
(defcustom proof-shell-annotated-prompt-regexp 1008,38265
(defcustom proof-shell-error-regexp 1023,38830
(defcustom proof-shell-truncate-before-error 1043,39632
(defcustom pg-next-error-regexp 1057,40171
(defcustom pg-next-error-filename-regexp 1072,40780
(defcustom pg-next-error-extract-filename 1096,41813
(defcustom proof-shell-interrupt-regexp 1103,42056
(defcustom proof-shell-proof-completed-regexp 1117,42651
(defcustom proof-shell-clear-response-regexp 1130,43159
(defcustom proof-shell-clear-goals-regexp 1142,43611
(defcustom proof-shell-start-goals-regexp 1154,44057
(defcustom proof-shell-end-goals-regexp 1162,44424
(defcustom proof-shell-eager-annotation-start 1176,44997
(defcustom proof-shell-eager-annotation-start-length 1199,46016
(defcustom proof-shell-eager-annotation-end 1210,46442
(defcustom proof-shell-strip-output-markup 1226,47117
(defcustom proof-shell-assumption-regexp 1235,47502
(defcustom proof-shell-process-file 1245,47906
(defcustom proof-shell-retract-files-regexp 1271,48982
(defcustom proof-shell-compute-new-files-list 1284,49470
(defcustom pg-special-char-regexp 1299,50037
(defcustom proof-shell-set-elisp-variable-regexp 1304,50181
(defcustom proof-shell-match-pgip-cmd 1342,51847
(defcustom proof-shell-issue-pgip-cmd 1356,52329
(defcustom proof-use-pgip-askprefs 1361,52494
(defcustom proof-shell-query-dependencies-cmd 1369,52841
(defcustom proof-shell-theorem-dependency-list-regexp 1376,53101
(defcustom proof-shell-theorem-dependency-list-split 1392,53761
(defcustom proof-shell-show-dependency-cmd 1401,54184
(defcustom proof-shell-trace-output-regexp 1423,55090
(defcustom proof-shell-thms-output-regexp 1441,55684
(defcustom proof-tokens-activate-command 1454,56067
(defcustom proof-tokens-deactivate-command 1461,56307
(defcustom proof-tokens-extra-modes 1468,56552
(defcustom proof-shell-unicode 1483,57057
(defcustom proof-shell-filename-escapes 1492,57447
(defcustom proof-shell-process-connection-type 1509,58127
(defcustom proof-shell-strip-crs-from-input 1515,58318
(defcustom proof-shell-strip-crs-from-output 1527,58801
(defcustom proof-shell-insert-hook 1535,59169
(defcustom proof-script-preprocess 1576,61129
(defcustom proof-shell-handle-delayed-output-hook1582,61280
(defcustom proof-shell-handle-error-or-interrupt-hook1588,61495
(defcustom proof-shell-pre-interrupt-hook1606,62241
(defcustom proof-shell-handle-output-system-specific 1614,62512
(defcustom proof-state-change-hook 1637,63485
(defcustom proof-shell-syntax-table-entries 1647,63878
(defgroup proof-goals 1665,64249
(defcustom pg-subterm-first-special-char 1670,64370
(defcustom pg-subterm-anns-use-stack 1678,64682
(defcustom pg-goals-change-goal 1687,64981
(defcustom pbp-goal-command 1692,65097
(defcustom pbp-hyp-command 1697,65253
(defcustom pg-subterm-help-cmd 1702,65415
(defcustom pg-goals-error-regexp 1709,65651
(defcustom proof-shell-result-start 1714,65811
(defcustom proof-shell-result-end 1720,66045
(defcustom pg-subterm-start-char 1726,66258
(defcustom pg-subterm-sep-char 1737,66732
(defcustom pg-subterm-end-char 1743,66911
(defcustom pg-topterm-regexp 1749,67068
(defcustom proof-goals-font-lock-keywords 1764,67668
(defcustom proof-response-font-lock-keywords 1772,68027
(defcustom proof-shell-font-lock-keywords 1780,68389
(defcustom pg-before-fontify-output-hook 1791,68903
(defcustom pg-after-fontify-output-hook 1799,69264

generic/proof-depends.el,917
(defvar proof-thm-names-of-files 25,639
(defvar proof-def-names-of-files 31,923
(defun proof-depends-module-name-for-buffer 42,1238
(defun proof-depends-module-of 52,1679
(defun proof-depends-names-in-same-file 60,1970
(defun proof-depends-process-dependencies 79,2578
(defun proof-dependency-in-span-context-menu 132,4313
(defun proof-dep-alldeps-menu 155,5203
(defun proof-dep-make-alldeps-menu 161,5429
(defun proof-dep-split-deps 179,5924
(defun proof-dep-make-submenu 198,6590
(defun proof-make-highlight-depts-menu 209,7001
(defun proof-goto-dependency 220,7309
(defun proof-show-dependency 227,7561
(defconst pg-dep-span-priority 234,7850
(defconst pg-ordinary-span-priority 235,7886
(defun proof-highlight-depcs 237,7928
(defun proof-highlight-depts 248,8394
(defun proof-depends-save-old-face 260,8904
(defun proof-depends-restore-old-face 265,9081
(defun proof-dep-unhighlight 271,9310

generic/proof-easy-config.el,192
(defconst proof-easy-config-derived-modes-table16,544
(defun proof-easy-config-define-derived-modes 23,950
(defun proof-easy-config-check-setup 52,2135
(defmacro proof-easy-config 84,3465

generic/proof-faces.el,1595
(defgroup proof-faces 29,809
(defconst pg-defface-window-systems36,989
(defmacro proof-face-specs 49,1551
(defface proof-queue-face64,2003
(defface proof-locked-face72,2281
(defface proof-declaration-name-face82,2602
(defface proof-tacticals-name-face91,2888
(defface proof-tactics-name-face100,3150
(defface proof-error-face109,3415
(defface proof-warning-face117,3636
(defface proof-eager-annotation-face126,3893
(defface proof-debug-message-face134,4111
(defface proof-boring-face142,4310
(defface proof-mouse-highlight-face150,4502
(defface proof-highlight-dependent-face158,4720
(defface proof-highlight-dependency-face166,4927
(defface proof-active-area-face174,5124
(defface proof-script-sticky-error-face182,5436
(defface proof-script-highlight-error-face190,5665
(defconst proof-face-compat-doc 202,6010
(defconst proof-queue-face 203,6090
(defconst proof-locked-face 204,6158
(defconst proof-declaration-name-face 205,6228
(defconst proof-tacticals-name-face 206,6318
(defconst proof-tactics-name-face 207,6404
(defconst proof-error-face 208,6486
(defconst proof-script-sticky-error-face 209,6554
(defconst proof-script-highlight-error-face 210,6650
(defconst proof-warning-face 211,6752
(defconst proof-eager-annotation-face 212,6824
(defconst proof-debug-message-face 213,6914
(defconst proof-boring-face 214,6998
(defconst proof-mouse-highlight-face 215,7068
(defconst proof-highlight-dependent-face 216,7156
(defconst proof-highlight-dependency-face 217,7252
(defconst proof-active-area-face 218,7350
(defconst proof-script-error-face 219,7430

generic/proof-indent.el,219
(defun proof-indent-indent 19,449
(defun proof-indent-offset 28,715
(defun proof-indent-inner-p 45,1316
(defun proof-indent-goto-prev 54,1616
(defun proof-indent-calculate 61,1949
(defun proof-indent-line 82,2708

generic/proof-maths-menu.el,83
(defun proof-maths-menu-set-global 32,906
(defun proof-maths-menu-enable 46,1357

generic/proof-menu.el,2026
(defvar proof-display-some-buffers-count 36,816
(defun proof-display-some-buffers 38,861
(defun proof-menu-define-keys 95,2988
(defun proof-menu-define-main 153,5808
(defvar proof-menu-favourites 162,5993
(defvar proof-menu-settings 165,6100
(defun proof-menu-define-specific 169,6189
(defun proof-assistant-menu-update 212,7451
(defvar proof-help-menu226,7884
(defvar proof-show-hide-menu234,8154
(defvar proof-buffer-menu245,8578
(defun proof-keep-response-history 308,10894
(defconst proof-quick-opts-menu316,11204
(defun proof-quick-opts-vars 514,19316
(defun proof-quick-opts-changed-from-defaults-p 546,20256
(defun proof-quick-opts-changed-from-saved-p 550,20361
(defun proof-quick-opts-save 561,20712
(defun proof-quick-opts-reset 566,20880
(defconst proof-config-menu578,21148
(defconst proof-advanced-menu585,21327
(defvar proof-menu603,22011
(defun proof-main-menu 612,22293
(defun proof-aux-menu 624,22632
(defun proof-menu-define-favourites-menu 640,22978
(defun proof-def-favourite 660,23627
(defvar proof-make-favourite-cmd-history 687,24620
(defvar proof-make-favourite-menu-history 690,24705
(defun proof-save-favourites 693,24791
(defun proof-del-favourite 698,24939
(defun proof-read-favourite 715,25495
(defun proof-add-favourite 739,26269
(defun proof-menu-define-settings-menu 766,27314
(defun proof-menu-entry-name 799,28445
(defun proof-menu-entry-for-setting 809,28795
(defun proof-settings-vars 828,29327
(defun proof-settings-changed-from-defaults-p 833,29504
(defun proof-settings-changed-from-saved-p 837,29610
(defun proof-settings-save 841,29713
(defun proof-settings-reset 846,29880
(defun proof-assistant-invisible-command-ifposs 851,30043
(defun proof-maybe-askprefs 873,31013
(defun proof-assistant-settings-cmd 879,31206
(defvar proof-assistant-format-table896,31861
(defun proof-assistant-format-bool 904,32231
(defun proof-assistant-format-int 907,32344
(defun proof-assistant-format-string 910,32436
(defun proof-assistant-format 913,32534

generic/proof-mmm.el,70
(defun proof-mmm-set-global 43,1439
(defun proof-mmm-enable 58,1978

generic/proof-script.el,5504
(deflocal proof-active-buffer-fake-minor-mode 45,1360
(deflocal proof-script-buffer-file-name 48,1486
(deflocal pg-script-portions 55,1896
(defun proof-next-element-count 65,2116
(defun proof-element-id 71,2358
(defun proof-next-element-id 75,2527
(deflocal proof-locked-span 111,3853
(deflocal proof-queue-span 118,4119
(deflocal proof-overlay-arrow 127,4605
(defun proof-span-give-warning 133,4732
(defun proof-span-read-only 139,4912
(defun proof-strict-read-only 148,5285
(defsubst proof-set-queue-endpoints 158,5663
(defun proof-set-overlay-arrow 162,5804
(defsubst proof-set-locked-endpoints 173,6142
(defsubst proof-detach-queue 178,6318
(defsubst proof-detach-locked 183,6457
(defsubst proof-set-queue-start 190,6682
(defsubst proof-set-locked-end 194,6808
(defsubst proof-set-queue-end 206,7278
(defun proof-init-segmentation 217,7575
(defun proof-colour-locked 249,8970
(defun proof-colour-locked-span 256,9243
(defun proof-sticky-errors 262,9516
(defun proof-restart-buffers 275,9932
(defun proof-script-buffers-with-spans 297,10751
(defun proof-script-remove-all-spans-and-deactivate 307,11107
(defun proof-script-clear-queue-spans-on-error 311,11297
(defun proof-script-delete-spans 337,12314
(defun proof-script-delete-secondary-spans 342,12513
(defun proof-unprocessed-begin 355,12802
(defun proof-script-end 363,13056
(defun proof-queue-or-locked-end 372,13366
(defun proof-locked-region-full-p 391,13959
(defun proof-locked-region-empty-p 400,14231
(defun proof-only-whitespace-to-locked-region-p 404,14381
(defun proof-in-locked-region-p 414,14730
(defun proof-goto-end-of-locked 426,14987
(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 443,15746
(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 455,16260
(defun proof-end-of-locked-visible-p 468,16844
(defvar pg-idioms 487,17437
(defun pg-clear-script-portions 490,17533
(defun pg-remove-element 496,17768
(defun pg-get-element 504,18071
(defun pg-add-element 514,18386
(defun pg-set-element-span-invisible 562,20365
(defun pg-open-invisible-span 566,20525
(defun pg-make-element-invisible 571,20696
(defun pg-make-element-visible 576,20907
(defun pg-toggle-element-span-visibility 581,21101
(defun pg-toggle-element-visibility 587,21264
(defun pg-show-all-portions 593,21527
(defun pg-show-all-proofs 612,22235
(defun pg-hide-all-proofs 617,22363
(defun pg-add-proof-element 622,22494
(defun pg-span-name 637,23265
(defvar pg-span-context-menu-keymap658,23965
(defun pg-last-output-displayform 665,24203
(defun pg-set-span-helphighlights 688,25094
(defun pg-delete-self-modification-hook 737,26908
(defun proof-complete-buffer-atomic 748,27181
(defun proof-register-possibly-new-processed-file789,29093
(defun proof-query-save-this-buffer-p 835,30967
(defun proof-inform-prover-file-retracted 840,31192
(defun proof-auto-retract-dependencies 860,32043
(defun proof-unregister-buffer-file-name 914,34593
(defun proof-protected-process-or-retract 960,36418
(defun proof-deactivate-scripting-auto 987,37588
(defun proof-deactivate-scripting 996,37946
(defun proof-activate-scripting 1129,43178
(defun proof-toggle-active-scripting 1229,47693
(defun proof-done-advancing 1268,48938
(defun proof-done-advancing-comment 1347,51923
(defun proof-done-advancing-save 1381,53299
(defun proof-make-goalsave1469,56663
(defun proof-get-name-from-goal 1487,57494
(defun proof-done-advancing-autosave 1507,58519
(defun proof-done-advancing-other 1572,61063
(defun proof-segment-up-to-parser 1601,61992
(defun proof-script-generic-parse-find-comment-end 1670,64258
(defun proof-script-generic-parse-cmdend 1679,64672
(defun proof-script-generic-parse-cmdstart 1730,66568
(defun proof-script-generic-parse-sexp 1769,68168
(defun proof-semis-to-vanillas 1781,68634
(defun proof-script-next-command-advance 1834,70307
(defun proof-assert-until-point 1853,70806
(defun proof-assert-electric-terminator 1868,71433
(defun proof-assert-semis 1903,72814
(defun proof-retract-before-change 1917,73555
(defun proof-inside-comment 1929,73956
(defun proof-inside-string 1935,74129
(defun proof-insert-pbp-command 1950,74409
(defun proof-insert-sendback-command 1965,74909
(defun proof-done-retracting 1991,75812
(defun proof-setup-retract-action 2026,77253
(defun proof-last-goal-or-goalsave 2036,77739
(defun proof-retract-target 2060,78651
(defun proof-retract-until-point-interactive 2142,82057
(defun proof-retract-until-point 2150,82442
(define-derived-mode proof-mode 2197,84275
(defun proof-script-set-visited-file-name 2233,85657
(defun proof-script-set-buffer-hooks 2255,86670
(defun proof-script-kill-buffer-fn 2263,87088
(defun proof-config-done-related 2295,88405
(defun proof-generic-goal-command-p 2366,91050
(defun proof-generic-state-preserving-p 2371,91263
(defun proof-generic-count-undos 2380,91780
(defun proof-generic-find-and-forget 2409,92833
(defconst proof-script-important-settings2460,94605
(defun proof-config-done 2475,95151
(defun proof-setup-parsing-mechanism 2536,97118
(defun proof-setup-imenu 2560,98197
(deflocal proof-segment-up-to-cache 2587,98975
(deflocal proof-segment-up-to-cache-start 2588,99016
(deflocal proof-last-edited-low-watermark 2589,99061
(defun proof-segment-up-to-using-cache 2599,99548
(defun proof-segment-cache-contents-for 2628,100682
(defun proof-script-after-change-function 2640,101051
(defun proof-script-set-after-change-functions 2652,101558

generic/proof-shell.el,3597
(defvar proof-marker 34,744
(defvar proof-action-list 37,840
(defsubst proof-shell-invoke-callback 56,1512
(defvar proof-shell-last-goals-output 70,2004
(defvar proof-shell-last-response-output 73,2084
(defvar proof-shell-delayed-output-start 76,2171
(defvar proof-shell-delayed-output-end 80,2353
(defvar proof-shell-delayed-output-flags 84,2533
(defvar proof-shell-interrupt-pending 87,2658
(defcustom proof-shell-active-scripting-indicator98,2953
(defun proof-shell-ready-prover 144,4312
(defsubst proof-shell-live-buffer 158,4851
(defun proof-shell-available-p 165,5090
(defun proof-grab-lock 171,5312
(defun proof-release-lock 181,5741
(defcustom proof-shell-fiddle-frames 191,5915
(defun proof-shell-set-text-representation 196,6073
(defun proof-shell-start 204,6401
(defvar proof-shell-kill-function-hooks 374,12125
(defun proof-shell-kill-function 377,12223
(defun proof-shell-clear-state 429,14024
(defun proof-shell-exit 445,14499
(defun proof-shell-bail-out 458,15003
(defun proof-shell-restart 468,15525
(defvar proof-shell-urgent-message-marker 510,16903
(defvar proof-shell-urgent-message-scanner 513,17024
(defun proof-shell-handle-error-output 517,17209
(defun proof-shell-handle-error-or-interrupt 543,18071
(defun proof-shell-error-or-interrupt-action 585,19774
(defun proof-goals-pos 608,20653
(defun proof-pbp-focus-on-first-goal 613,20864
(defsubst proof-shell-string-match-safe 625,21280
(defun proof-shell-handle-immediate-output 629,21441
(defun proof-interrupt-process 696,24048
(defun proof-shell-insert 729,25236
(defun proof-shell-action-list-item 780,27062
(defun proof-shell-set-silent 785,27304
(defun proof-shell-start-silent-item 791,27523
(defun proof-shell-clear-silent 797,27712
(defun proof-shell-stop-silent-item 803,27934
(defsubst proof-shell-should-be-silent 809,28123
(defsubst proof-shell-insert-action-item 820,28633
(defsubst proof-shell-slurp-comments 824,28808
(defun proof-add-to-queue 835,29213
(defun proof-start-queue 893,31237
(defun proof-extend-queue 904,31631
(defun proof-shell-exec-loop 918,32099
(defun proof-shell-insert-loopback-cmd 986,34402
(defun proof-shell-process-urgent-message 1011,35566
(defun proof-shell-process-urgent-message-default 1060,37286
(defun proof-shell-process-urgent-message-trace 1076,37870
(defun proof-shell-process-urgent-message-retract 1089,38429
(defun proof-shell-process-urgent-message-elisp 1110,39277
(defun proof-shell-process-urgent-message-thmdeps 1125,39772
(defun proof-shell-strip-eager-annotations 1139,40151
(defun proof-shell-filter 1155,40651
(defun proof-shell-filter-first-command 1255,44023
(defun proof-shell-process-urgent-messages 1270,44566
(defun proof-shell-filter-manage-output 1320,46132
(defsubst proof-shell-display-output-as-response 1352,47379
(defun proof-shell-handle-delayed-output 1358,47671
(defvar pg-last-tracing-output-time 1453,51130
(defconst pg-slow-mode-duration 1456,51236
(defconst pg-fast-tracing-mode-threshold 1459,51318
(defvar pg-tracing-cleanup-timer 1462,51446
(defun pg-tracing-tight-loop 1464,51485
(defun pg-finish-tracing-display 1507,53197
(defun proof-shell-wait 1525,53561
(defun proof-done-invisible 1555,54766
(defun proof-shell-invisible-command 1561,54936
(defun proof-shell-invisible-cmd-get-result 1608,56505
(defun proof-shell-invisible-command-invisible-result 1620,56941
(defun pg-insert-last-output-as-comment 1640,57442
(define-derived-mode proof-shell-mode 1659,57914
(defconst proof-shell-important-settings1696,58941
(defun proof-shell-config-done 1702,59056

generic/proof-site.el,503
(defconst proof-assistant-table-default26,771
(defconst proof-general-short-version64,2168
(defconst proof-general-version-year 70,2355
(defgroup proof-general 77,2508
(defgroup proof-general-internals 82,2616
(defun proof-home-directory-fn 95,3004
(defcustom proof-home-directory106,3376
(defcustom proof-images-directory115,3742
(defcustom proof-info-directory121,3944
(defcustom proof-assistant-table150,4921
(defcustom proof-assistants 185,6034
(defun proof-ready-for-assistant 214,7190

generic/proof-splash.el,991
(defcustom proof-splash-enable 34,1007
(defcustom proof-splash-time 39,1159
(defcustom proof-splash-contents47,1443
(defconst proof-splash-startup-msg91,3008
(defconst proof-splash-welcome 100,3386
(define-derived-mode proof-splash-mode 103,3490
(define-key proof-splash-mode-map 109,3664
(define-key proof-splash-mode-map 110,3716
(defsubst proof-emacs-imagep 115,3843
(defun proof-get-image 120,3968
(defvar proof-splash-timeout-conf 142,4768
(defun proof-splash-centre-spaces 145,4881
(defun proof-splash-remove-screen 170,5966
(defun proof-splash-remove-buffer 187,6622
(defvar proof-splash-seen 198,7010
(defun proof-splash-insert-contents 201,7112
(defun proof-splash-display-screen 241,8242
(defalias 'pg-about pg-about
277,9764
(defun proof-splash-message 280,9830
(defun proof-splash-timeout-waiter 293,10274
(defvar proof-splash-old-frame-title-format 306,10832
(defun proof-splash-set-frame-titles 308,10882
(defun proof-splash-unset-frame-titles 317,11197

generic/proof-syntax.el,1061
(defsubst proof-ids-to-regexp 22,517
(defsubst proof-anchor-regexp 29,755
(defconst proof-no-regexp 33,860
(defsubst proof-regexp-alt 36,951
(defsubst proof-re-search-forward-region 45,1263
(defsubst proof-search-forward 58,1761
(defsubst proof-replace-regexp-in-string 65,2031
(defsubst proof-re-search-forward 70,2282
(defsubst proof-re-search-backward 75,2540
(defsubst proof-re-search-forward-safe 80,2801
(defsubst proof-string-match 86,3082
(defsubst proof-string-match-safe 91,3311
(defsubst proof-stringfn-match 95,3515
(defsubst proof-looking-at 102,3778
(defsubst proof-looking-at-safe 107,3965
(defsubst proof-looking-at-syntactic-context-default 111,4110
(defsubst proof-replace-string 122,4487
(defsubst proof-replace-regexp 127,4691
(defsubst proof-replace-regexp-nocasefold 132,4900
(defvar proof-id 140,5182
(defsubst proof-ids 146,5402
(defun proof-zap-commas 153,5654
(defadvice font-lock-fontify-keywords-region179,6540
(defun proof-format 195,7136
(defun proof-format-filename 214,7775
(defun proof-insert 261,9177

generic/proof-toolbar.el,2332
(defun proof-toolbar-function 33,810
(defun proof-toolbar-icon 37,957
(defun proof-toolbar-enabler 41,1104
(defun proof-toolbar-make-icon 50,1306
(defun proof-toolbar-make-toolbar-items 59,1614
(defvar proof-toolbar-map 84,2419
(defun proof-toolbar-available-p 87,2518
(defun proof-toolbar-setup 97,2824
(defun proof-toolbar-enable 118,3681
(defalias 'proof-toolbar-undo proof-toolbar-undo
151,4739
(defun proof-toolbar-undo-enable-p 153,4807
(defalias 'proof-toolbar-delete proof-toolbar-delete
160,4965
(defun proof-toolbar-delete-enable-p 162,5046
(defalias 'proof-toolbar-home proof-toolbar-home
170,5228
(defalias 'proof-toolbar-next proof-toolbar-next
174,5295
(defun proof-toolbar-next-enable-p 176,5366
(defalias 'proof-toolbar-goto proof-toolbar-goto
182,5482
(defun proof-toolbar-goto-enable-p 184,5532
(defalias 'proof-toolbar-retract proof-toolbar-retract
189,5617
(defun proof-toolbar-retract-enable-p 191,5674
(defalias 'proof-toolbar-use proof-toolbar-use
197,5793
(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
198,5845
(defalias 'proof-toolbar-restart proof-toolbar-restart
202,5926
(defalias 'proof-toolbar-goal proof-toolbar-goal
206,5991
(defalias 'proof-toolbar-qed proof-toolbar-qed
210,6049
(defun proof-toolbar-qed-enable-p 212,6098
(defalias 'proof-toolbar-state proof-toolbar-state
220,6260
(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
221,6303
(defalias 'proof-toolbar-context proof-toolbar-context
225,6382
(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
226,6428
(defalias 'proof-toolbar-command proof-toolbar-command
230,6509
(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
231,6565
(defun proof-toolbar-help 235,6670
(defalias 'proof-toolbar-find proof-toolbar-find
241,6750
(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
242,6802
(defalias 'proof-toolbar-info proof-toolbar-info
246,6877
(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p
247,6932
(defalias 'proof-toolbar-visibility proof-toolbar-visibility
251,7030
(defun proof-toolbar-visibility-enable-p 253,7090
(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
258,7204
(defun proof-toolbar-interrupt-enable-p 259,7265
(defun proof-toolbar-scripting-menu 267,7418

generic/proof-unicode-tokens.el,497
(defvar proof-unicode-tokens-initialised 31,827
(defun proof-unicode-tokens-init 34,934
(defun proof-unicode-tokens-configure 48,1436
(defun proof-unicode-tokens-mode-if-enabled 60,1882
(defun proof-unicode-tokens-set-global 66,2081
(defun proof-unicode-tokens-enable 82,2651
(defun proof-unicode-tokens-reconfigure 102,3504
(defun proof-unicode-tokens-configure-prover 128,4392
(defun proof-unicode-tokens-activate-prover 133,4573
(defun proof-unicode-tokens-deactivate-prover 140,4819

generic/proof-useropts.el,1635
(defgroup proof-user-options 21,559
(defun proof-set-value 29,738
(defcustom proof-electric-terminator-enable 62,1861
(defcustom proof-toolbar-enable 74,2393
(defcustom proof-imenu-enable 80,2566
(defcustom pg-show-hints 86,2737
(defcustom proof-shell-quiet-errors 91,2870
(defcustom proof-trace-output-slow-catchup 98,3141
(defcustom proof-strict-state-preserving 108,3638
(defcustom proof-strict-read-only 121,4247
(defcustom proof-three-window-enable 134,4826
(defcustom proof-multiple-frames-enable 153,5576
(defcustom proof-delete-empty-windows 162,5909
(defcustom proof-shrink-windows-tofit 173,6440
(defcustom proof-auto-raise-buffers 180,6712
(defcustom proof-colour-locked 187,6947
(defcustom proof-sticky-errors 195,7197
(defcustom proof-query-file-save-when-activating-scripting202,7414
(defcustom proof-one-command-per-line218,8134
(defcustom proof-prog-name-ask225,8358
(defcustom proof-prog-name-guess231,8518
(defcustom proof-tidy-response239,8783
(defcustom proof-keep-response-history253,9246
(defcustom pg-input-ring-size 263,9634
(defcustom proof-general-debug 268,9786
(defcustom proof-use-parser-cache 277,10157
(defcustom proof-follow-mode 284,10413
(defcustom proof-auto-action-when-deactivating-scripting 308,11590
(defcustom proof-script-command-separator 331,12539
(defcustom proof-rsh-command 339,12831
(defcustom proof-disappearing-proofs 355,13381
(defcustom proof-full-annotation 360,13542
(defcustom proof-minibuffer-messages 369,13912
(defcustom proof-autosend-enable 377,14221
(defcustom proof-autosend-delay 383,14401
(defcustom proof-fast-process-buffer 389,14559

generic/proof-utils.el,1568
(defmacro proof-with-current-buffer-if-exists 61,1730
(defmacro proof-with-script-buffer 70,2107
(defmacro proof-map-buffers 81,2488
(defmacro proof-sym 86,2673
(defsubst proof-try-require 91,2834
(defun proof-save-some-buffers 104,3165
(defun proof-save-this-buffer 124,3761
(defun proof-file-truename 137,4125
(defun proof-files-to-buffers 141,4307
(defun proof-buffers-in-mode 149,4546
(defun pg-save-from-death 163,4996
(defun proof-define-keys 182,5612
(defun pg-remove-specials 193,5897
(defun pg-remove-specials-in-string 203,6233
(defun proof-warn-if-unset 214,6459
(defun proof-get-window-for-buffer 219,6677
(defun proof-display-and-keep-buffer 270,8985
(defun proof-clean-buffer 312,10708
(defun pg-internal-warning 328,11364
(defun proof-debug 336,11646
(defun proof-switch-to-buffer 346,12017
(defun proof-resize-window-tofit 368,13141
(defun proof-submit-bug-report 463,16989
(defun proof-deftoggle-fn 498,18346
(defmacro proof-deftoggle 513,19009
(defun proof-defintset-fn 520,19385
(defmacro proof-defintset 536,20089
(defun proof-defstringset-fn 543,20468
(defmacro proof-defstringset 556,21094
(defun proof-escape-keymap-doc 569,21550
(defmacro proof-defshortcut 573,21704
(defmacro proof-definvisible 588,22302
(defun pg-custom-save-vars 615,23231
(defun pg-custom-reset-vars 631,23875
(defun proof-locate-executable 644,24212
(defun pg-current-word-pos 659,24767
(defun proof-looking-at-syntactic-context 706,26483
(defsubst proof-shell-strip-output-markup 721,27051
(defun proof-minibuffer-message 727,27315

lib/bufhist.el,1257
(defun bufhist-ring-update 38,1391
(defgroup bufhist 47,1713
(defcustom bufhist-ring-size 51,1794
(defvar bufhist-ring 56,1905
(defvar bufhist-ring-pos 59,1979
(defvar bufhist-lastswitch-modified-tick 62,2058
(defvar bufhist-read-only-history 65,2164
(defvar bufhist-saved-mode-line-format 68,2235
(defvar bufhist-normal-read-only 71,2338
(defvar bufhist-top-point 74,2432
(defun bufhist-mode-line-format-entry 77,2522
(defconst bufhist-minor-mode-map106,3596
(define-minor-mode bufhist-mode119,4073
(defun bufhist-get-buffer-contents 141,4954
(defun bufhist-restore-buffer-contents 150,5296
(defun bufhist-checkpoint 159,5610
(defun bufhist-erase-buffer 167,5979
(defun bufhist-checkpoint-and-erase 178,6350
(defun bufhist-switch-to-index 184,6536
(defun bufhist-first 223,8135
(defun bufhist-last 228,8294
(defun bufhist-prev 233,8438
(defun bufhist-next 241,8661
(defun bufhist-delete 246,8801
(defun bufhist-clear 258,9342
(defun bufhist-init 273,9737
(defun bufhist-exit 301,10746
(defun bufhist-set-readwrite 311,11010
(defun bufhist-before-change-function 326,11630
(define-button-type 'bufhist-nextbufhist-next
340,12053
(define-button-type 'bufhist-prevbufhist-prev
344,12150
(defun bufhist-insert-buttons 351,12362

lib/holes.el,2465
(defvar holes-default-hole 44,1121
(defvar holes-active-hole 50,1299
(defgroup holes 60,1496
(defcustom holes-empty-hole-string 65,1595
(defcustom holes-empty-hole-regexp 70,1738
(defface active-hole-face92,2440
(defface inactive-hole-face102,2856
(defvar hole-map116,3297
(defvar holes-mode-map126,3688
(defun holes-region-beginning-or-nil 172,5425
(defun holes-region-end-or-nil 176,5561
(defun holes-copy-active-region 180,5679
(defun holes-is-hole-p 186,5889
(defun holes-hole-start-position 190,5981
(defun holes-hole-end-position 196,6164
(defun holes-hole-buffer 201,6335
(defun holes-hole-at 207,6509
(defun holes-active-hole-exist-p 212,6679
(defun holes-active-hole-start-position 219,6932
(defun holes-active-hole-end-position 227,7300
(defun holes-active-hole-buffer 236,7663
(defun holes-goto-active-hole 244,7964
(defun holes-highlight-hole-as-active 253,8223
(defun holes-highlight-hole 261,8531
(defun holes-disable-active-hole 269,8818
(defun holes-set-active-hole 282,9350
(defun holes-is-in-hole-p 292,9695
(defun holes-make-hole 296,9833
(defun holes-make-hole-at 314,10489
(defun holes-clear-hole 328,10942
(defun holes-clear-hole-at 337,11200
(defun holes-map-holes 345,11456
(defun holes-clear-all-buffer-holes 349,11610
(defun holes-next 359,11911
(defun holes-next-after-active-hole 366,12163
(defun holes-set-active-hole-next 373,12379
(defun holes-replace-segment 392,12916
(defun holes-replace 401,13269
(defun holes-replace-active-hole 429,14447
(defun holes-replace-update-active-hole 436,14738
(defun holes-delete-update-active-hole 454,15385
(defun holes-set-make-active-hole 462,15612
(defalias 'holes-track-mouse-selection holes-track-mouse-selection
477,16167
(defsubst holes-track-mouse-clicks 478,16225
(defun holes-mouse-replace-active-hole 482,16335
(defun holes-destroy-hole 496,16806
(defsubst holes-hole-at-event 510,17188
(defun holes-mouse-destroy-hole 514,17288
(defun holes-mouse-forget-hole 521,17509
(defun holes-mouse-set-make-active-hole 531,17801
(defun holes-mouse-set-active-hole 547,18300
(defun holes-set-point-next-hole-destroy 556,18551
(defun holes-replace-string-by-holes-backward 582,19532
(defun holes-skeleton-end-hook 600,20232
(defconst holes-jump-doc609,20670
(defun holes-replace-string-by-holes-backward-jump 616,20876
(define-minor-mode holes-mode 633,21558
(defun holes-abbrev-complete 728,25040
(defun holes-insert-and-expand 738,25383

lib/local-vars-list.el,373
(defconst local-vars-list-doc 28,825
(defun local-vars-list-insert-empty-zone 44,1387
(defun local-vars-list-find 82,2090
(defun local-vars-list-goto-var 101,2861
(defun local-vars-list-get-current 127,3908
(defun local-vars-list-set-current 148,4758
(defun local-vars-list-get 171,5473
(defun local-vars-list-get-safe 188,6003
(defun local-vars-list-set 193,6197

lib/maths-menu.el,242
(defvar maths-menu-filter-predicate 56,2317
(defvar maths-menu-tokenise-insert 59,2426
(defun maths-menu-build-menu 62,2563
(defvar maths-menu-menu84,3324
(defvar maths-menu-mode-map344,12882
(define-minor-mode maths-menu-mode352,13101

lib/pg-dev.el,199
(defconst pg-dev-lisp-font-lock-keywords52,1588
(defun pg-loadpath 80,2422
(defun unload-pg 90,2593
(defun profile-pg 121,3487
(defun elp-pack-number 150,4514
(defun pg-bug-references 159,4714

lib/pg-fontsets.el,209
(defcustom pg-fontsets-default-fontset 24,722
(defvar pg-fontsets-names 29,868
(defun pg-fontsets-make-fontsetsizes 32,949
(defconst pg-fontsets-base-fonts51,1710
(defun pg-fontsets-make-fontsets 57,1840

lib/proof-compat.el,297
(defvar proof-running-on-win32 32,975
(defun pg-custom-undeclare-variable 53,1777
(defmacro save-selected-frame 85,2548
(defun proof-buffer-syntactic-context-emulate 95,2925
(defalias 'proof-buffer-syntactic-contextproof-buffer-syntactic-context
164,5213
(defmacro declare-function 179,5596

lib/scomint.el,876
(defface scomint-highlight-input 19,493
(defface scomint-highlight-prompt23,609
(defvar scomint-buffer-maximum-size 30,847
(defvar scomint-output-filter-functions 35,1038
(defvar scomint-mode-map39,1149
(defvar scomint-last-input-start 45,1328
(defvar scomint-last-input-end 46,1366
(defvar scomint-last-output-start 47,1402
(defvar scomint-exec-hook 49,1442
(define-derived-mode scomint-mode 59,1824
(defsubst scomint-check-proc 78,2739
(defun scomint-make-in-buffer 86,3079
(defun scomint-make 110,4346
(defun scomint-exec 123,5057
(defun scomint-exec-1 160,6650
(defalias 'scomint-send-string scomint-send-string
210,8780
(defun scomint-send-eof 212,8834
(defun scomint-send-input 221,9067
(defun scomint-truncate-buffer 264,10568
(defun scomint-strip-ctrl-m 277,10962
(defun scomint-output-filter 291,11525
(defun scomint-interrupt-process 363,14257

lib/span.el,1361
(defalias 'span-start span-start
22,609
(defalias 'span-end span-end
23,647
(defalias 'span-set-property span-set-property
24,681
(defalias 'span-property span-property
25,724
(defalias 'span-make span-make
26,763
(defalias 'span-detach span-detach
27,799
(defalias 'span-set-endpoints span-set-endpoints
28,839
(defalias 'span-buffer span-buffer
29,884
(defun span-read-only-hook 31,925
(defsubst span-read-only 36,1115
(defsubst span-read-write 43,1425
(defsubst span-write-warning 48,1595
(defsubst span-lt 59,2119
(defsubst spans-at-point-prop 64,2263
(defsubst spans-at-region-prop 73,2454
(defsubst span-at 83,2720
(defsubst span-delete 87,2846
(defsubst span-mapcar-spans 94,3068
(defsubst span-mapc-spans 98,3243
(defsubst span-mapcar-spans-inorder 102,3414
(defun span-at-before 108,3619
(defsubst prev-span 125,4343
(defsubst next-span 131,4496
(defsubst span-live-p 137,4710
(defsubst span-raise 143,4876
(defsubst span-string 147,5009
(defsubst set-span-properties 152,5169
(defsubst span-find-span 158,5363
(defsubst span-at-event 166,5675
(defun fold-spans 172,5872
(defsubst span-detached-p 186,6405
(defsubst set-span-face 190,6521
(defsubst set-span-keymap 194,6619
(defsubst span-delete-spans 202,6788
(defsubst span-property-safe 206,6950
(defsubst span-set-start 210,7087
(defsubst span-set-end 214,7219

lib/texi-docstring-magic.el,584
(defun texi-docstring-magic-find-face 88,3027
(defun texi-docstring-magic-splice-sep 93,3192
(defconst texi-docstring-magic-munge-table103,3497
(defun texi-docstring-magic-untabify 193,7260
(defun texi-docstring-magic-munge-docstring 200,7458
(defun texi-docstring-magic-texi 239,8739
(defun texi-docstring-magic-format-default 252,9179
(defun texi-docstring-magic-texi-for 268,9812
(defconst texi-docstring-magic-comment326,11771
(defun texi-docstring-magic 332,11925
(defun texi-docstring-magic-face-at-point 366,13004
(defun texi-docstring-magic-insert-magic 381,13527

lib/unicode-chars.el,80
(defvar unicode-chars-alist12,348
(defun unicode-chars-list-chars 5051,245975

lib/unicode-tokens.el,5900
(defgroup unicode-tokens-options 55,1712
(defcustom unicode-tokens-add-help-echo 60,1837
(defun unicode-tokens-toggle-add-help-echo 65,2004
(defvar unicode-tokens-token-symbol-map 79,2410
(defvar unicode-tokens-token-format 98,3069
(defvar unicode-tokens-token-variant-format-regexp 104,3318
(defvar unicode-tokens-shortcut-alist 118,3851
(defvar unicode-tokens-shortcut-replacement-alist 124,4128
(defvar unicode-tokens-control-region-format-regexp 132,4334
(defvar unicode-tokens-control-char-format-regexp 139,4702
(defvar unicode-tokens-control-regions 146,5063
(defvar unicode-tokens-control-characters 149,5139
(defvar unicode-tokens-control-char-format 152,5221
(defvar unicode-tokens-control-region-format-start 155,5334
(defvar unicode-tokens-control-region-format-end 158,5451
(defvar unicode-tokens-tokens-customizable-variables 161,5564
(defconst unicode-tokens-configuration-variables168,5732
(defun unicode-tokens-config 183,6131
(defun unicode-tokens-config-var 187,6276
(defun unicode-tokens-copy-configuration-variables 199,6716
(defvar unicode-tokens-token-list 227,7932
(defvar unicode-tokens-hash-table 230,8052
(defvar unicode-tokens-token-match-regexp 233,8168
(defvar unicode-tokens-uchar-hash-table 239,8451
(defvar unicode-tokens-uchar-regexp 243,8638
(defgroup unicode-tokens-faces 251,8823
(defconst unicode-tokens-font-family-alternatives261,9120
(defface unicode-tokens-symbol-font-face276,9617
(defface unicode-tokens-script-font-face286,9975
(defface unicode-tokens-fraktur-font-face291,10119
(defface unicode-tokens-serif-font-face296,10244
(defface unicode-tokens-sans-font-face301,10381
(defface unicode-tokens-highlight-face306,10503
(defconst unicode-tokens-fonts315,10865
(defconst unicode-tokens-fontsymb-properties324,11082
(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map
352,12698
(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist
370,13250
(defconst unicode-tokens-font-lock-extra-managed-props383,13581
(defun unicode-tokens-font-lock-keywords 387,13735
(defun unicode-tokens-calculate-token-match 420,15106
(defun unicode-tokens-usable-composition 450,16142
(defun unicode-tokens-help-echo 463,16521
(defvar unicode-tokens-show-symbols 468,16723
(defun unicode-tokens-interpret-composition 471,16837
(defun unicode-tokens-font-lock-compose-symbol 489,17349
(defun unicode-tokens-prepend-text-properties-in-match 527,18881
(defun unicode-tokens-prepend-text-property 541,19459
(defun unicode-tokens-show-symbols 566,20604
(defun unicode-tokens-symbs-to-props 574,20914
(defvar unicode-tokens-show-controls 594,21613
(defun unicode-tokens-show-controls 597,21704
(defun unicode-tokens-control-char 609,22217
(defun unicode-tokens-control-region 618,22656
(defun unicode-tokens-control-font-lock-keywords 629,23203
(defvar unicode-tokens-use-shortcuts 640,23527
(defun unicode-tokens-use-shortcuts 643,23630
(defun unicode-tokens-map-ordering 659,24226
(defun unicode-tokens-quail-define-rules 668,24579
(defun unicode-tokens-insert-token 691,25256
(defun unicode-tokens-annotate-region 700,25560
(defun unicode-tokens-insert-control 724,26398
(defun unicode-tokens-insert-uchar-as-token 734,26847
(defun unicode-tokens-delete-token-near-point 740,27068
(defun unicode-tokens-delete-backward-char 752,27509
(defun unicode-tokens-delete-char 763,27890
(defun unicode-tokens-delete-backward-1 774,28244
(defun unicode-tokens-delete-1 791,28848
(defun unicode-tokens-prev-token 807,29392
(defun unicode-tokens-rotate-token-forward 815,29689
(defun unicode-tokens-rotate-token-backward 842,30579
(defun unicode-tokens-replace-shortcut-match 847,30781
(defun unicode-tokens-replace-shortcuts 856,31151
(defun unicode-tokens-replace-unicode-match 870,31749
(defun unicode-tokens-replace-unicode 877,32050
(defun unicode-tokens-copy-token 894,32649
(define-button-type 'unicode-tokens-listunicode-tokens-list
901,32870
(defun unicode-tokens-list-tokens 907,33074
(defun unicode-tokens-list-shortcuts 946,34258
(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars
964,34896
(defun unicode-tokens-encode-in-temp-buffer 966,34969
(defun unicode-tokens-encode 984,35625
(defun unicode-tokens-encode-str 990,35861
(defun unicode-tokens-copy 994,36023
(defun unicode-tokens-paste 1003,36429
(defvar unicode-tokens-highlight-unicode 1022,37150
(defconst unicode-tokens-unicode-highlight-patterns1025,37242
(defun unicode-tokens-highlight-unicode 1029,37411
(defun unicode-tokens-highlight-unicode-setkeywords 1041,37874
(defun unicode-tokens-initialise 1053,38243
(defvar unicode-tokens-mode-map 1073,38914
(defvar unicode-tokens-display-table1076,39011
(define-minor-mode unicode-tokens-mode1083,39262
(defun unicode-tokens-set-font-var 1216,43745
(defun unicode-tokens-set-font-var-aux 1232,44234
(defun unicode-tokens-mouse-set-font 1263,45395
(defsubst unicode-tokens-face-font-sym 1276,45909
(defun unicode-tokens-set-font-restart 1280,46089
(defun unicode-tokens-save-fonts 1291,46399
(defun unicode-tokens-custom-save-faces 1299,46655
(define-key unicode-tokens-mode-map1316,47111
(define-key unicode-tokens-mode-map1319,47218
(defvar unicode-tokens-quail-translation-keymap1323,47308
(define-key unicode-tokens-quail-translation-keymap1330,47498
(defun unicode-tokens-quail-delete-last-char 1334,47632
(define-key unicode-tokens-mode-map 1349,48059
(define-key unicode-tokens-mode-map 1351,48151
(define-key unicode-tokens-mode-map1353,48242
(define-key unicode-tokens-mode-map1355,48348
(define-key unicode-tokens-mode-map1358,48463
(define-key unicode-tokens-mode-map1360,48572
(define-key unicode-tokens-mode-map1362,48680
(define-key unicode-tokens-mode-map1364,48786
(defun unicode-tokens-customize-submenu 1372,48910
(defun unicode-tokens-define-menu 1379,49133

mmm/mmm-auto.el,343
(defvar mmm-autoloaded-classes67,2676
(defun mmm-autoload-class 89,3439
(defvar mmm-changed-buffers-list 129,4992
(defun mmm-major-mode-change 132,5099
(defun mmm-check-changed-buffers 145,5620
(defun mmm-mode-on-maybe 154,5970
(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks
166,6374
(defun mmm-add-find-file-hook 167,6434

mmm/mmm-class.el,415
(defun mmm-get-class-spec 42,1296
(defun mmm-get-class-parameter 59,1939
(defun mmm-set-class-parameter 63,2105
(defun* mmm-apply-class75,2455
(defun* mmm-apply-classes90,3072
(defun* mmm-apply-all 110,3803
(defun* mmm-ify124,4250
(defun* mmm-match-region206,7095
(defun mmm-match->point 269,9480
(defun mmm-match-and-verify 284,10050
(defun mmm-get-form 310,11101
(defun mmm-default-get-form 321,11576

mmm/mmm-cmds.el,712
(defun mmm-ify-by-class 41,1210
(defun mmm-ify-region 63,1822
(defun mmm-ify-by-regexp75,2243
(defun mmm-parse-buffer 97,2886
(defun mmm-parse-region 106,3222
(defun mmm-parse-block 115,3601
(defun mmm-get-block 132,4352
(defun mmm-reparse-current-region 146,4634
(defun mmm-clear-current-region 167,5210
(defun mmm-clear-regions 172,5374
(defun mmm-clear-all-regions 177,5520
(defun* mmm-end-current-region 185,5680
(defun mmm-narrow-to-submode-region 220,6928
(defun mmm-insert-region 239,7542
(defun mmm-insert-by-key 258,8348
(defun mmm-get-insertion-spec 342,11613
(defun mmm-insertion-help 369,12573
(defun mmm-display-insertion-key 379,12936
(defun mmm-get-all-insertion-keys 401,13723

mmm/mmm-compat.el,418
(defvar mmm-xemacs 40,1313
(defvar mmm-keywords-used49,1616
(defmacro mmm-regexp-opt 91,2632
(defvar mmm-evaporate-property110,3281
(defmacro mmm-set-keymap-default 128,4047
(defmacro mmm-event-key 137,4489
(defvar skeleton-positions 146,4708
(defun mmm-fixup-skeleton 147,4739
(defmacro mmm-make-temp-buffer 159,5162
(defvar mmm-font-lock-available-p 172,5558
(defmacro mmm-set-font-lock-defaults 179,5772

mmm/mmm-cweb.el,228
(defvar mmm-cweb-section-tags38,1117
(defvar mmm-cweb-section-regexp41,1164
(defvar mmm-cweb-c-part-tags44,1254
(defvar mmm-cweb-c-part-regexp47,1313
(defun mmm-cweb-in-limbo 50,1397
(defun mmm-cweb-verify-brief-c 57,1622

mmm/mmm-mason.el,410
(defvar mmm-mason-perl-tags41,1236
(defvar mmm-mason-pseudo-perl-tags45,1377
(defvar mmm-mason-non-perl-tags48,1453
(defvar mmm-mason-perl-tags-regexp51,1554
(defvar mmm-mason-pseudo-perl-tags-regexp56,1749
(defvar mmm-mason-tag-names-regexp61,1966
(defun mmm-mason-verify-inline 66,2186
(defun mmm-mason-start-line 156,4838
(defun mmm-mason-end-line 161,4903
(defun mmm-mason-set-mode-line 168,4997

mmm/mmm-mode.el,1023
(defun mmm-mode 101,3867
(defun mmm-mode-on 140,5372
(defun mmm-mode-off 181,7048
(defvar mmm-mode-map 206,7760
(defvar mmm-mode-prefix-map 209,7835
(defvar mmm-mode-menu-map 212,7945
(defun mmm-define-key 215,8036
(define-key mmm-mode-prefix-map 239,8791
(define-key mmm-mode-prefix-map 246,9049
(define-key mmm-mode-map 249,9160
(define-key mmm-mode-menu-map 252,9262
(define-key mmm-mode-menu-map 254,9334
(define-key mmm-mode-menu-map 256,9393
(define-key mmm-mode-menu-map 258,9474
(define-key mmm-mode-menu-map 260,9555
(define-key mmm-mode-menu-map 262,9642
(define-key mmm-mode-menu-map 265,9736
(define-key mmm-mode-menu-map 267,9796
(define-key mmm-mode-menu-map 270,9887
(define-key mmm-mode-menu-map 272,9947
(define-key mmm-mode-menu-map 274,10054
(define-key mmm-mode-menu-map 276,10139
(define-key mmm-mode-menu-map 279,10225
(define-key mmm-mode-menu-map 281,10285
(define-key mmm-mode-menu-map 283,10398
(define-key mmm-mode-menu-map 285,10483
(define-key mmm-mode-map 288,10566

mmm/mmm-region.el,1643
(defsubst mmm-overlay-at 54,1749
(defun mmm-overlays-at 59,1934
(defun mmm-included-p 72,2387
(defun mmm-overlays-containing 112,3876
(defun mmm-overlays-contained-in 125,4314
(defun mmm-overlays-overlapping 138,4754
(defun mmm-sort-overlays 149,5117
(defvar mmm-current-overlay 158,5359
(defvar mmm-previous-overlay 163,5574
(defvar mmm-current-submode 168,5762
(defvar mmm-previous-submode 173,5962
(defun mmm-update-current-submode 178,6135
(defun mmm-set-current-submode 199,6930
(defun mmm-submode-at 210,7373
(defun mmm-match-front 219,7648
(defun mmm-match-back 238,8409
(defun mmm-front-start 257,9154
(defun mmm-back-end 265,9458
(defun mmm-valid-submode-region 278,9805
(defun* mmm-make-region305,10961
(defun mmm-make-overlay 431,16311
(defun mmm-get-face 459,17444
(defun mmm-clear-overlays 470,17736
(defun mmm-update-mode-info 486,18201
(defun mmm-update-submode-region 571,21841
(defun mmm-add-hooks 588,22571
(defun mmm-remove-hooks 591,22668
(defun mmm-get-local-variables-list 597,22795
(defun mmm-get-locals 617,23491
(defun mmm-get-saved-local 630,23988
(defun mmm-set-local-variables 634,24153
(defun mmm-get-saved-local-variables 645,24531
(defun mmm-save-changed-local-variables 653,24806
(defun mmm-clear-local-variables 672,25510
(defun mmm-enable-font-lock 683,25775
(defun mmm-update-font-lock-buffer 691,26035
(defun mmm-refontify-maybe 704,26446
(defun mmm-submode-changes-in 719,26926
(defun mmm-regions-in 730,27283
(defun mmm-regions-alist 744,27761
(defun mmm-fontify-region 761,28288
(defun mmm-fontify-region-list 781,29284
(defun mmm-beginning-of-syntax 803,30032

mmm/mmm-rpm.el,154
(defconst mmm-rpm-sh-start-tags48,1618
(defvar mmm-rpm-sh-end-tags53,1842
(defvar mmm-rpm-sh-start-regexp57,2016
(defvar mmm-rpm-sh-end-regexp61,2194

mmm/mmm-sample.el,168
(defvar mmm-here-doc-mode-alist 84,2601
(defun mmm-here-doc-get-mode 93,3086
(defun mmm-file-variables-verify 208,6343
(defun mmm-file-variables-find-back 232,7148

mmm/mmm-univ.el,34
(defun mmm-univ-get-mode 38,1205

mmm/mmm-utils.el,282
(defmacro mmm-valid-buffer 42,1332
(defmacro mmm-save-all 61,1941
(defun mmm-format-string 74,2223
(defun mmm-format-matches 85,2661
(defmacro mmm-save-keyword 108,3419
(defmacro mmm-save-keywords 116,3746
(defun mmm-looking-back-at 129,4244
(defun mmm-make-marker 146,4784

mmm/mmm-vars.el,2668
(defgroup mmm 104,3283
(defvar mmm-c-derived-modes111,3393
(defvar mmm-save-local-variables115,3512
(defvar mmm-buffer-saved-locals 341,10293
(defvar mmm-region-saved-locals-defaults 346,10493
(defvar mmm-region-saved-locals-for-dominant 352,10753
(defgroup mmm-faces 362,11130
(defcustom mmm-submode-decoration-level 368,11301
(defface mmm-init-submode-face 386,12145
(defface mmm-cleanup-submode-face 390,12285
(defface mmm-declaration-submode-face 394,12422
(defface mmm-comment-submode-face 398,12568
(defface mmm-output-submode-face 402,12721
(defface mmm-special-submode-face 406,12870
(defface mmm-code-submode-face 410,13034
(defface mmm-default-submode-face 414,13173
(defface mmm-delimiter-face 419,13381
(defcustom mmm-mode-string 426,13507
(defcustom mmm-submode-mode-line-format 431,13638
(defvar mmm-primary-mode-display-name 448,14293
(defvar mmm-buffer-mode-display-name 453,14507
(defun mmm-set-mode-line 459,14806
(defvar mmm-classes 483,15614
(defvar mmm-global-classes 489,15859
(defcustom mmm-mode-ext-classes-alist 496,16041
(defun mmm-add-mode-ext-class 515,16831
(defcustom mmm-major-mode-preferences524,17156
(defun mmm-add-to-major-mode-preferences 542,17884
(defun mmm-ensure-modename 558,18642
(defun mmm-modename->function 567,18945
(defcustom mmm-delimiter-mode 581,19394
(defcustom mmm-mode-prefix-key 591,19663
(defcustom mmm-command-modifiers 596,19790
(defcustom mmm-insert-modifiers 610,20423
(defcustom mmm-use-old-command-keys 625,21101
(defun mmm-use-old-command-keys 635,21565
(defcustom mmm-mode-hook 643,21757
(defun mmm-run-constructed-hook 663,22564
(defun mmm-run-major-hook 671,22908
(defun mmm-run-submode-hook 674,22985
(defvar mmm-class-hooks-run 677,23072
(defun mmm-run-class-hook 682,23244
(defvar mmm-primary-mode-entry-hook 687,23416
(defcustom mmm-major-mode-hook 702,24063
(defun mmm-run-major-mode-hook 716,24694
(defcustom mmm-global-mode 729,25235
(defcustom mmm-never-modes745,25902
(defvar mmm-set-file-name-for-modes 763,26202
(defvar mmm-mode 774,26561
(defvar mmm-primary-mode 782,26769
(defvar mmm-classes-alist 793,27135
(defun mmm-add-classes 948,35342
(defun mmm-add-group 953,35507
(defun mmm-add-to-group 963,35880
(defconst mmm-version 977,36307
(defun mmm-version 980,36372
(defvar mmm-temp-buffer-name 987,36515
(defvar mmm-interactive-history 993,36645
(defun mmm-add-to-history 999,36914
(defun mmm-clear-history 1002,36997
(defvar mmm-mode-ext-classes 1010,37182
(defun mmm-get-mode-ext-classes 1015,37393
(defun mmm-clear-mode-ext-classes 1024,37720
(defun mmm-mode-ext-applies 1028,37845
(defun mmm-get-all-classes 1042,38224

doc/ProofGeneral.texi,6304
@node Top161,4909
@node Preface199,6063
@node News for Version 4.0News for Version 4.0
222,6652
@node Future243,7447
@node Credits272,8782
@node Introducing Proof GeneralIntroducing Proof General
391,12966
@node Installing Proof GeneralInstalling Proof General
446,14940
@node Quick start guideQuick start guide
460,15389
@node Features of Proof GeneralFeatures of Proof General
504,17510
@node Supported proof assistantsSupported proof assistants
593,21447
@node Prerequisites for this manualPrerequisites for this manual
642,23338
@node Organization of this manualOrganization of this manual
686,24957
@node Basic Script ManagementBasic Script Management
712,25785
@node Walkthrough example in IsabelleWalkthrough example in Isabelle
731,26385
@node Proof scriptsProof scripts
997,36637
@node Script buffersScript buffers
1040,38757
@node Locked queue and editing regionsLocked queue and editing regions
1062,39334
@node Goal-save sequencesGoal-save sequences
1118,41481
@node Active scripting bufferActive scripting buffer
1155,42947
@node Summary of Proof General buffersSummary of Proof General buffers
1224,46367
@node Script editing commandsScript editing commands
1273,48624
@node Script processing commandsScript processing commands
1353,51582
@node Proof assistant commandsProof assistant commands
1480,56875
@node Toolbar commandsToolbar commands
1655,63070
@node Interrupting during trace outputInterrupting during trace output
1679,63999
@node Advanced Script Management and EditingAdvanced Script Management and Editing
1719,65929
@node Document centred workingDocument centred working
1740,66550
@node Automatic processingAutomatic processing
1809,69143
@node Visibility of completed proofsVisibility of completed proofs
1838,70152
@node Switching between proof scriptsSwitching between proof scripts
1893,72081
@node View of processed files View of processed files 
1930,74053
@node Retracting across filesRetracting across files
1990,77104
@node Asserting across filesAsserting across files
2003,77735
@node Automatic multiple file handlingAutomatic multiple file handling
2016,78301
@node Escaping script managementEscaping script management
2041,79335
@node Editing featuresEditing features
2098,81447
@node Unicode symbols and special layout supportUnicode symbols and special layout support
2168,84226
@node Maths menuMaths menu
2210,85784
@node Unicode Tokens modeUnicode Tokens mode
2227,86475
@node Configuring tokens symbols and shortcutsConfiguring tokens symbols and shortcuts
2277,88898
@node Special layout Special layout 
2307,89859
@node Moving between Unicode and tokensMoving between Unicode and tokens
2415,93975
@node Finding available tokens shortcuts and symbolsFinding available tokens shortcuts and symbols
2470,96086
@node Selecting suitable fontsSelecting suitable fonts
2509,97260
@node Support for other PackagesSupport for other Packages
2574,100235
@node Syntax highlightingSyntax highlighting
2604,101071
@node Imenu and SpeedbarImenu and Speedbar
2632,102074
@node Support for outline modeSupport for outline mode
2678,103730
@node Support for completionSupport for completion
2703,104859
@node Support for tagsSupport for tags
2760,107021
@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
2812,109369
@node Goals buffer commandsGoals buffer commands
2827,109881
@node Customizing Proof GeneralCustomizing Proof General
2915,113416
@node Basic optionsBasic options
2955,115086
@node How to customizeHow to customize
2979,115856
@node Display customizationDisplay customization
3026,117823
@node User optionsUser options
3180,124228
@node Changing facesChanging faces
3411,132414
@node Script buffer facesScript buffer faces
3433,133289
@node Goals and response facesGoals and response faces
3479,134889
@node Tweaking configuration settingsTweaking configuration settings
3524,136421
@node Hints and TipsHints and Tips
3581,138947
@node Adding your own keybindingsAdding your own keybindings
3600,139548
@node Using file variablesUsing file variables
3664,142162
@node Using abbreviationsUsing abbreviations
3723,144348
@node LEGO Proof GeneralLEGO Proof General
3762,145763
@node LEGO specific commandsLEGO specific commands
3803,147132
@node LEGO tagsLEGO tags
3823,147587
@node LEGO customizationsLEGO customizations
3833,147834
@node Coq Proof GeneralCoq Proof General
3865,148753
@node Coq-specific commandsCoq-specific commands
3881,149162
@node Coq-specific variablesCoq-specific variables
3903,149669
@node Editing multiple proofsEditing multiple proofs
3925,150327
@node User-loaded tacticsUser-loaded tactics
3949,151435
@node Holes featureHoles feature
4013,153909
@node Isabelle Proof GeneralIsabelle Proof General
4040,155196
@node Choosing logic and starting isabelleChoosing logic and starting isabelle
4066,156072
@node Isabelle commandsIsabelle commands
4135,158873
@node Isabelle settingsIsabelle settings
4278,163065
@node Isabelle customizationsIsabelle customizations
4292,163647
@node HOL Proof GeneralHOL Proof General
4315,164134
@node Shell Proof GeneralShell Proof General
4357,165956
@node Obtaining and InstallingObtaining and Installing
4393,167415
@node Obtaining Proof GeneralObtaining Proof General
4408,167780
@node Installing Proof General from tarballInstalling Proof General from tarball
4434,168662
@node Setting the names of binariesSetting the names of binaries
4458,169452
@node Notes for syssiesNotes for syssies
4486,170392
@node Bugs and EnhancementsBugs and Enhancements
4562,173389
@node References4583,174204
@node History of Proof GeneralHistory of Proof General
4623,175227
@node Old News for 3.0Old News for 3.0
4717,179392
@node Old News for 3.1Old News for 3.1
4787,183086
@node Old News for 3.2Old News for 3.2
4813,184258
@node Old News for 3.3Old News for 3.3
4874,187261
@node Old News for 3.4Old News for 3.4
4893,188158
@node Old News for 3.5Old News for 3.5
4915,189213
@node Old News for 3.6Old News for 3.6
4919,189270
@node Old News for 3.7Old News for 3.7
4924,189370
@node Function IndexFunction Index
4968,191293
@node Variable IndexVariable Index
4972,191369
@node Keystroke IndexKeystroke Index
4976,191449
@node Concept IndexConcept Index
4980,191515

doc/PG-adapting.texi,3770
@node Top153,4679
@node Introduction190,5788
@node Future231,7441
@node Credits267,9037
@node Beginning with a New ProverBeginning with a New Prover
277,9329
@node Overview of adding a new proverOverview of adding a new prover
317,11271
@node Demonstration instance and easy configurationDemonstration instance and easy configuration
394,14577
@node Major modes used by Proof GeneralMajor modes used by Proof General
463,17968
@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
506,19678
@node Settings for generic user-level commandsSettings for generic user-level commands
521,20224
@node Menu configurationMenu configuration
566,21956
@node Toolbar configurationToolbar configuration
590,22873
@node Proof Script SettingsProof Script Settings
649,25110
@node Recognizing commands and commentsRecognizing commands and comments
671,25690
@node Recognizing proofsRecognizing proofs
808,32127
@node Recognizing other elementsRecognizing other elements
912,36441
@node Configuring undo behaviourConfiguring undo behaviour
975,38920
@node Nested proofsNested proofs
1112,44307
@node Safe (state-preserving) commandsSafe (state-preserving) commands
1152,45933
@node Activate scripting hookActivate scripting hook
1175,46886
@node Automatic multiple filesAutomatic multiple files
1199,47756
@node Completions1221,48603
@node Proof Shell SettingsProof Shell Settings
1262,50093
@node Proof shell commandsProof shell commands
1293,51375
@node Script input to the shellScript input to the shell
1457,58419
@node Settings for matching various output from proof processSettings for matching various output from proof process
1525,61489
@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1647,66845
@node Hooks and other settingsHooks and other settings
1887,77603
@node Goals Buffer SettingsGoals Buffer Settings
1972,81116
@node Splash Screen SettingsSplash Screen Settings
2046,84106
@node Global ConstantsGlobal Constants
2072,84861
@node Handling Multiple FilesHandling Multiple Files
2098,85690
@node Configuring Editing SyntaxConfiguring Editing Syntax
2250,93473
@node Configuring Font LockConfiguring Font Lock
2307,95590
@node Configuring TokensConfiguring Tokens
2379,99084
@node Writing More Lisp CodeWriting More Lisp Code
2429,101204
@node Default values for generic settingsDefault values for generic settings
2446,101849
@node Adding prover-specific configurationsAdding prover-specific configurations
2476,102932
@node Useful variablesUseful variables
2519,104214
@node Useful functions and macrosUseful functions and macros
2534,104713
@node Internals of Proof GeneralInternals of Proof General
2643,108936
@node Spans2673,109866
@node Proof General site configurationProof General site configuration
2688,110239
@node Configuration variable mechanismsConfiguration variable mechanisms
2771,113336
@node Global variablesGlobal variables
2897,118810
@node Proof script modeProof script mode
2972,121413
@node Proof shell modeProof shell mode
3201,131722
@node Debugging3698,151547
@node Plans and IdeasPlans and Ideas
3741,152423
@node Proof by pointing and similar featuresProof by pointing and similar features
3762,153145
@node Granularity of atomic command sequencesGranularity of atomic command sequences
3800,154803
@node Browser mode for script files and theoriesBrowser mode for script files and theories
3845,157028
@node Demonstration InstantiationsDemonstration Instantiations
3875,158059
@node demoisa-easy.el3891,158490
@node demoisa.el3953,160682
@node Function IndexFunction Index
4107,165622
@node Variable IndexVariable Index
4111,165698
@node Concept IndexConcept Index
4120,165877

generic/proof.el,0

pgshell/pgshell.el,0

isar/isar-profiling.el,0

isar/interface-setup.el,0

demoisa/demoisa-easy.el,0

coq/coq-mmm.el,0

coq/coq-autotest.el,0

acl2/acl2.el,0