Print startup banners so the text fits into the lines of hyphens

HOL-Theorem-Prover · Jun 29, 2023 · 2120b03 · 2120b03
1 parent bcc1c3a
commit 2120b03
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git a/std.prelude b/std.prelude
@@ -165,12 +165,12 @@ struct
   fun print_banner() =
     TextIO.output(TextIO.stdOut,
      "\n---------------------------------------------------------------------\n"
-     ^"       HOL-4 ["
+     ^"     HOL4 ["
      ^Globals.release^" "^Lib.int_to_string(Globals.version)
      ^" ("^Thm.kernelid^", "^build_stamp
      ^")]\n\n"
-     ^"       For introductory HOL help, type: help \"hol\";\n"
-     ^"       "^exit_string
+     ^"     For introductory HOL help, type: help \"hol\";\n"
+     ^"     "^exit_string
      ^"\n---------------------------------------------------------------------\
       \\n\n")
 

diff --git a/tools-poly/holinteractive.ML b/tools-poly/holinteractive.ML
@@ -41,7 +41,7 @@ struct
     end
     handle _ => ""
   val id_string =
-    "HOL-4 [" ^ Globals.release ^ " " ^ Lib.int_to_string Globals.version ^
+    "HOL4 [" ^ Globals.release ^ " " ^ Lib.int_to_string Globals.version ^
     " (" ^ Thm.kernelid ^ ", " ^ build_stamp ^ ")]\n\n"
   val exit_string =
     if Systeml.OS = "winNT" then
@@ -54,9 +54,9 @@ struct
   fun print_banner () =
     TextIO.output (TextIO.stdOut,
       line ^
-      "       " ^ id_string ^
-      "       For introductory HOL help, type: help \"hol\";\n" ^
-      "       " ^ exit_string ^
+      "     " ^ id_string ^
+      "     For introductory HOL help, type: help \"hol\";\n" ^
+      "     " ^ exit_string ^
       line)
 end;