src/Pure/Thy/thy_scan.ML
changeset 2025 9acc10ac1e1d
parent 1512 ce37c64244c0
child 2151 000767995143
equal deleted inserted replaced
2024:909153d8318f 2025:9acc10ac1e1d