src/Pure/Thy/thy_header.ML
changeset 43279 6af741899bf6
parent 42003 6e45dc518ebb
child 44160 8848867501fb
equal deleted inserted replaced
43278:1fbdcebb364b 43279:6af741899bf6