aboutsummaryrefslogtreecommitdiffhomepage
path: root/hol-light/hol-light-unicode-tokens.el
diff options
context:
space:
mode:
Diffstat (limited to 'hol-light/hol-light-unicode-tokens.el')
-rw-r--r--hol-light/hol-light-unicode-tokens.el19
1 files changed, 15 insertions, 4 deletions
diff --git a/hol-light/hol-light-unicode-tokens.el b/hol-light/hol-light-unicode-tokens.el
index df32e4bd..7e24e4b1 100644
--- a/hol-light/hol-light-unicode-tokens.el
+++ b/hol-light/hol-light-unicode-tokens.el
@@ -1,8 +1,17 @@
-;;; -*- coding: utf-8; -*-
-;; coq-unicode-tokens.el --- (No) Tokens for Unicode Tokens package
-;;
-;; Copyright(C) 2012 David Aspinall / University of Edinburgh
+;;; coq-unicode-tokens.el --- (No) Tokens for Unicode Tokens package -*- coding: utf-8; -*-
+
+;; 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>
+
+;;; Commentary:
;;
;; This file is loaded by `proof-unicode-tokens.el'.
;;
@@ -18,6 +27,8 @@
;; - fix unicode tokens sorting so longs tokens handled first (broken?)
;; <=> not <= >
+;;; Code:
+
(require 'proof-unicode-tokens)
(defconst hol-light-token-format "%s") ; plain tokens