src/Pure/ML/ml_print_depth0.ML
Thu, 07 Apr 2016 13:54:02 +0200 wenzelm simplified default print_depth: context is usually available, in contrast to 0d295e339f52;
Tue, 05 Apr 2016 20:51:37 +0200 wenzelm clarified modules -- simplified bootstrap;
less more (0) tip