src/Pure/General/print_mode.ML
changeset 24150 ed724867099a
parent 24058 81aafd465662
child 24362 a9fe7ed25fa4