src/Pure/Syntax/syntax.ML
changeset 58839 ccda99401bc8
parent 58047 9f3826352b52
child 58978 e42da880c61e
equal deleted inserted replaced
58838:59203adfc33f 58839:ccda99401bc8