src/Pure/General/print_mode.ML
changeset 24762 8d7da66b1a2c
parent 24634 38db11874724
child 25118 158149a6e95b