src/Pure/Syntax/syntax_ext.ML
changeset 59545 12a6088ed195
parent 58854 b979c781c2db
child 59841 2551ac44150e
equal deleted inserted replaced
59544:792691e4b311 59545:12a6088ed195