src/Pure/Syntax/syntax.ML
changeset 4701 be8a8d60d962
parent 4618 731bed12f762
child 4703 a50ab39756db