src/Pure/Syntax/syntax.ML
changeset 19423 51eeee99bd8f
parent 19375 8198a4ffff24
child 19482 9f11af8f7ef9