changeset 11704 | 3c50a2cd6f00 |
parent 10969 | cfd85f5c6eac |
child 24105 | af364e2b4048 |
1.1 --- a/src/HOL/Unix/ROOT.ML Fri Oct 05 23:58:52 2001 +0200 1.2 +++ b/src/HOL/Unix/ROOT.ML Sat Oct 06 00:02:46 2001 +0200 1.3 @@ -1,3 +1,3 @@ 1.4 1.5 -Library.setmp print_mode (! print_mode @ ["no_brackets"]) 1.6 +Library.setmp print_mode (! print_mode @ ["no_brackets", "no_type_brackets"]) 1.7 use_thy "Unix";