src/Pure/General/print_mode.ML
changeset 36016 4f5c7a19ebe0
parent 33223 d27956b4d3b4
child 37146 f652333bbf8e