This file is indexed.

/usr/share/hol88-2.02.19940316/lisp/banner.l is in hol88-source 2.02.19940316-28.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below.

 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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;                             HOL 88 Version 2.1                          ;;;
;;;                                                                         ;;;
;;;   FILE NAME:        banner.l                                            ;;;
;;;                                                                         ;;;
;;;   DESCRIPTION:      HOL system banner                                   ;;;
;;;                                                                         ;;;
;;;   USES FILES:       f-franz.l (or f-cl.l)                               ;;;
;;;                                                                         ;;;
;;;                     University of Cambridge                             ;;;
;;;                     Hardware Verification Group                         ;;;
;;;                     Computer Laboratory                                 ;;;
;;;                     New Museums Site                                    ;;;
;;;                     Pembroke Street                                     ;;;
;;;                     Cambridge  CB2 3QG                                  ;;;
;;;                     England                                             ;;;
;;;                                                                         ;;;
;;;   COPYRIGHT:        University of Edinburgh                             ;;;
;;;   COPYRIGHT:        University of Cambridge                             ;;;
;;;   COPYRIGHT:        INRIA                                               ;;;
;;;                                                                         ;;;
;;;   REVISION HISTORY: "Classic HOL" banner added by MJCG on 31 March 1992 ;;;
;;;                     ========== banner installed by MJCG on 27 June 1992 ;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(eval-when (compile)
   #+franz (include "lisp/f-franz")
   (special %build-date %version))


;;;(setq HOL-sym
;;;  `|_  _         __        _         
;;;!__!        !  !       !
;;;!  ! IGHER  !__! RDER  !__ OGIC
;;;===============================
;;;|)

;;;(defconstant HOL-sym
;;;"          _  _    __    _      __    __
;;;   |___   |__|   |  |   |     |__|  |__|
;;;   |      |  |   |__|   |__   |__|  |__|
;;;   
;;;")

;;;(defconstant HOL-sym
;;;"           __  _     _    __   __  _   __     _  _   __   _
;;;   |___   |    |    /_\\  |__  |__  |  |       |__|  |  |  |
;;;   |      |__  |__ /   \\  __|  __| |  |__     |  |  |__|  |__
;;;
;;;")

(defconstant eqline
"
===============================================================================
")

(setq %build-date (date))

;;; Version: set in Makefile
(setq %version '"<version number>")

(defun banner ()
   (terpri)
   (princ eqline)
   (princ "         HOL88 Version ") (princ %version) 
   (princ '", built on ") (princ %build-date)
   (princ eqline)
   )


;;;(defun banner ()
;;;   (terpri)
;;;   (princ HOL-sym)
;;;   (princ "          HOL88 Version ") (princ %version) 
;;;   (princ '", built on ") (princ %build-date)
;;;   (terpri)
;;;   )

;;;(defun banner ()
;;;       (terpri)
;;;       (princ '|Higher Order Logic|) (terpri)
;;;       (princ '|==================|) (terpri)
;;;       (princ `|[Based on Cambridge LCF, version |)
;;;       (princ %version)
;;;       (princ '|  created |) (princ %ctime) (princ '|]|) (terpri)
;;;       (cond (experimental (princ '|Experimental system!|) (terpri)))
;;; )