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