src/Pure/Syntax/syntax.ML
changeset 58910 edcd9339bda1
parent 58047 9f3826352b52
child 58978 e42da880c61e