src/HOL/ROOT.ML
changeset 3947 eb707467f8c5
parent 3578 b2b9a9ddb9cc
child 3981 b4f93a8da835
     1.1 --- a/src/HOL/ROOT.ML	Mon Oct 20 11:22:29 1997 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Mon Oct 20 11:25:39 1997 +0200
     1.3 @@ -7,9 +7,11 @@
     1.4  Should be executed in the subdirectory HOL.
     1.5  *)
     1.6  
     1.7 -val banner = "Higher-Order Logic with curried functions";
     1.8 +val banner = "Higher-Order Logic";
     1.9  writeln banner;
    1.10  
    1.11 +reset global_names;
    1.12 +
    1.13  print_depth 1;
    1.14  
    1.15  (* Add user sections *)