src/Pure/Syntax/syntax_ext.ML
changeset 79233 f0e49c3957a9
parent 77999 ec850750db87
child 80748 43c4817375bf
equal deleted inserted replaced
79232:99bc2dd45111 79233:f0e49c3957a9