src/HOL/ROOT.ML
changeset 4024 3c056eab237c
parent 3981 b4f93a8da835
child 4088 9be9e39fd862
     1.1 --- a/src/HOL/ROOT.ML	Tue Oct 28 17:37:46 1997 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Tue Oct 28 17:41:15 1997 +0100
     1.3 @@ -10,8 +10,6 @@
     1.4  val banner = "Higher-Order Logic";
     1.5  writeln banner;
     1.6  
     1.7 -reset global_names;
     1.8 -
     1.9  print_depth 1;
    1.10  
    1.11  (* Add user sections *)