blob: 3187f32c8f1d322aac7010cc7ec3f7567816225e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
;;; proof.el --- Proof General loader.
;;
;; Copyright (C) 1998-2008 LFCS Edinburgh.
;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen,
;; Thomas Kleymann and Dilip Sequeira
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; $Id$
;;
;;; Commentary:
;;
;; This file loads Proof General. It is required by the
;; individual prover modes. Loading order of PG is:
;;
;; 1. proof-site (autoloads & stubs for mode functions)
;; 2. autoload of <PA>/<PA>.el by auto-mode-alist
;; 3. <PA>.el requires this file
;; 4. rest of PG loaded here, inc proof-config/pg-custom
;; 5. further modules loaded by autoloads.
;;
;;; Code:
(require 'proof-site) ; site/prover config, global vars
(require 'proof-autoloads) ; autoloaded functions
(require 'proof-compat) ; Emacs and OS compatibility
(require 'proof-utils) ; utilities
(require 'proof-config) ; configuration variables
(proof-splash-message) ; welcome the user now.
(provide 'proof)
;;; proof.el ends here
|
