src/HOL/Unix/ROOT.ML
changeset 10969 cfd85f5c6eac
parent 10966 8f2c27041a8e
child 11704 3c50a2cd6f00
     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";