src/Pure/General/print_mode.ML
changeset 82582 bcee022fbe30
parent 80869 87395be1a299