src/Pure/Syntax/syntax.ML
changeset 43004 20e9caff1f86
parent 42820 3daff3cc2214
child 43558 94a08fb3ae4a