changeset 62978 | c04eead96cca |
parent 62900 | c641bf9402fd |
child 64556 | 851ae0e7b09c |
--- a/src/Pure/ML/ml_print_depth.ML Thu Apr 14 12:17:44 2016 +0200 +++ b/src/Pure/ML/ml_print_depth.ML Thu Apr 14 15:33:23 2016 +0200 @@ -1,4 +1,4 @@ -(* Title: Pure/ML/ml_print_depth0.ML +(* Title: Pure/ML/ml_print_depth.ML Author: Makarius Print depth for ML toplevel pp: context option with global default.