src/Pure/Syntax/syntax.ML
changeset 42889 412fe70f41a4
parent 42820 3daff3cc2214
child 43558 94a08fb3ae4a