author | wenzelm |
Tue, 31 Jul 2007 22:21:22 +0200 | |
changeset 24105 | af364e2b4048 |
parent 24104 | 719fbe4fb77f |
child 24106 | f2965bf954dc |
--- a/src/HOL/Unix/ROOT.ML Tue Jul 31 22:21:20 2007 +0200 +++ b/src/HOL/Unix/ROOT.ML Tue Jul 31 22:21:22 2007 +0200 @@ -1,3 +1,4 @@ +(* $Id$ *) -Library.setmp print_mode (! print_mode @ ["no_brackets", "no_type_brackets"]) +setmp_noncritical print_mode (! print_mode @ ["no_brackets", "no_type_brackets"]) use_thy "Unix";