src/Pure/General/print_mode.ML
changeset 33205 20587741a8d9
parent 32738 15bb09ca0378
child 33223 d27956b4d3b4