src/Pure/Syntax/syntax_ext.ML
changeset 64061 1bbea2b55d22
parent 63933 e149e3e320a3
child 64677 8dc24130e8fe