aboutsummaryrefslogtreecommitdiffhomepage
path: root/hol-light/hol-light.el
diff options
context:
space:
mode:
Diffstat (limited to 'hol-light/hol-light.el')
-rw-r--r--hol-light/hol-light.el21
1 files changed, 15 insertions, 6 deletions
diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el
index 467453ed..2b4f3989 100644
--- a/hol-light/hol-light.el
+++ b/hol-light/hol-light.el
@@ -1,15 +1,24 @@
-;; hol-light.el Basic Proof General instance for HOL Light
-;;
-;; Copyright (C) 2010-12 LFCS Edinburgh, David Aspinall.
-;;
+;;; hol-light.el --- Basic Proof General instance for HOL Light
+
+;; This file is part of Proof General.
+
+;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
+;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc.
+;; Portions © Copyright 2001-2017 Pierre Courtieu
+;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
+;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
+;; Portions © Copyright 2015-2017 Clément Pit-Claudel
+
;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
;; Mark Adams <mark@proof-technologies.com>
-;;
-;; $Id$
+
+;;; Commentary:
;;
;; See the README file in this directory for information.
;;
+;;; Code:
+
(require 'proof-easy-config) ; easy configure mechanism
(require 'proof-syntax) ; functions for making regexps