src/Pure/Syntax/syntax.ML
changeset 36944 dbf831a50e4a
parent 36739 e9401d2efc5f
child 37146 f652333bbf8e