src/Pure/General/print_mode.ML
changeset 25111 d52a58b51f1f
parent 24634 38db11874724
child 25118 158149a6e95b