src/Pure/Syntax/syntax.ML
changeset 4273 c9b577c8f7a1
parent 4145 ffb0c9670597
child 4487 9b4c1db5aca1
equal deleted inserted replaced
4272:61c6ae12ca14 4273:c9b577c8f7a1