no_brackets;
authorwenzelm
Wed Jan 24 00:06:32 2001 +0100 (2001-01-24)
changeset 10969cfd85f5c6eac
parent 10968 4882d65cc716
child 10970 7917e66505a4
no_brackets;
src/HOL/Unix/ROOT.ML
     1.1 --- a/src/HOL/Unix/ROOT.ML	Tue Jan 23 18:17:14 2001 +0100
     1.2 +++ b/src/HOL/Unix/ROOT.ML	Wed Jan 24 00:06:32 2001 +0100
     1.3 @@ -1,2 +1,3 @@
     1.4  
     1.5 -use_thy "Unix";
     1.6 +Library.setmp print_mode (! print_mode @ ["no_brackets"])
     1.7 +  use_thy "Unix";