src/Pure/Thy/thy_output.ML
changeset 47625 10cfaf771687
parent 47005 421760a1efe7
child 48918 6e5fd4585512
equal deleted inserted replaced
47624:16d433895d2e 47625:10cfaf771687