src/Pure/Syntax/syntax.ML
changeset 15992 cb02d70a2040
parent 15833 78109c7012ed
child 16613 76e57e08dcb5
equal deleted inserted replaced
15991:670f8e4b5a98 15992:cb02d70a2040