src/Doc/Implementation/Syntax.thy
changeset 58837 e84d900cd287
parent 58618 782f0b662cae
child 61416 b9a3324e4e62