src/Pure/Syntax/syntax.ML
changeset 28962 f603183f7a5c
parent 28904 3ef9489eeef5
child 29004 a5a91f387791
equal deleted inserted replaced
28961:9f33ab8e15db 28962:f603183f7a5c