src/Pure/Thy/thy_output.ML
changeset 23214 dc23c062b58c
parent 22124 27b674312b2f
child 23272 25c84ca5e9a9
equal deleted inserted replaced
23213:43553703267c 23214:dc23c062b58c