src/Pure/Syntax/syntax.ML
changeset 512 55755ed9fab9
parent 383 fcea89074e4c
child 556 3f5f42467717