src/Pure/Syntax/syntax.ML
changeset 4130 9fac2370a2f4
parent 4101 e8ad51c88be9
child 4145 ffb0c9670597