src/Pure/Syntax/syntax.ML
changeset 2210 8369f3f4bb4f
parent 2202 cc15a7bfbe12
child 2287 94b70aeb7d1f