src/Pure/Syntax/syntax.ML
changeset 19346 c4c003abd830
parent 19300 7689f81f8996
child 19375 8198a4ffff24