src/Pure/Syntax/syntax.ML
changeset 24857 2dde4189a055
parent 24768 123e219b66c2
child 24923 9e095546cdac