src/Pure/Syntax/syntax.ML
changeset 2404 edcc26b1461d
parent 2383 4127499d9b52
child 2504 f5e2288c2697
equal deleted inserted replaced
2403:8115988ccc22 2404:edcc26b1461d