src/Pure/Syntax/syntax.ML
changeset 69836 9b4901bda2a7
parent 69589 e15f053a42d8
child 69971 4e98239aa083
equal deleted inserted replaced
69835:b1dfaa25130e 69836:9b4901bda2a7