src/Pure/General/print_mode.ML
changeset 24854 0ebcd575d3c6
parent 24634 38db11874724
child 25118 158149a6e95b