changeset 62978 | c04eead96cca |
parent 62900 | c641bf9402fd |
child 64556 | 851ae0e7b09c |
62974:f17602cbf76a | 62978:c04eead96cca |
---|---|
1 (* Title: Pure/ML/ml_print_depth0.ML |
1 (* Title: Pure/ML/ml_print_depth.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Print depth for ML toplevel pp: context option with global default. |
4 Print depth for ML toplevel pp: context option with global default. |
5 *) |
5 *) |
6 |
6 |