src/Pure/General/output_primitives_virtual.ML
2016-04-09 wenzelm 2016-04-09 shared output primitives of physical/virtual Pure;