# HG changeset patch
# User paulson
# Date 865246584 -7200
# Node ID 2a2def2ac317a6cc27b41f285b23e21eb78180a5
# Parent  f59e64fe4058b16820e8430b3cc0834a7f7f878a
Corrected banner: it is W0, not MiniML

diff -r f59e64fe4058 -r 2a2def2ac317 src/HOL/W0/ROOT.ML
--- a/src/HOL/W0/ROOT.ML	Mon Jun 02 12:15:13 1997 +0200
+++ b/src/HOL/W0/ROOT.ML	Mon Jun 02 12:16:24 1997 +0200
@@ -8,7 +8,7 @@
 
 HOL_build_completed;    (*Make examples fail if HOL did*)
 
-writeln"Root file for HOL/MiniML";
+writeln"Root file for HOL/W0";
 Unify.trace_bound := 20;
 
 AddSEs [less_SucE];