src/Pure/Syntax/syntax.ML
changeset 69740 18d383f41477
parent 69589 e15f053a42d8
child 69971 4e98239aa083