src/Pure/General/print_mode.ML
changeset 33178 70522979c7be
parent 32738 15bb09ca0378
child 33223 d27956b4d3b4