src/Pure/General/output.ML
changeset 56800 b904ea8edd73
parent 56334 6b3739fee456
child 56830 e760242101fc
equal deleted inserted replaced
56799:00b13fb87b3a 56800:b904ea8edd73