src/Pure/Thy/thy_output.ML
changeset 72638 2a7fc87495e0
parent 71507 39fa41148890
child 73687 54fe8cc0e1c6
equal deleted inserted replaced
72637:fd68c9c1b90b 72638:2a7fc87495e0