src/Pure/General/output_primitives_virtual.ML
changeset 83004 304519f22c2c
parent 82316 83584916b6d7