src/Doc/Implementation/Syntax.thy
changeset 58839 ccda99401bc8
parent 58618 782f0b662cae
child 61416 b9a3324e4e62