src/Pure/Syntax/syntax.ML
changeset 69655 2b56cbb02e8a
parent 69589 e15f053a42d8
child 69971 4e98239aa083