src/Pure/General/output.ML
changeset 55672 5e25cc741ab9
parent 55387 51f0876f61df
child 56297 3925634718fb
equal deleted inserted replaced
55671:aeca05e62fef 55672:5e25cc741ab9