src/Doc/Implementation/Syntax.thy
changeset 59886 e0dc738eb08c
parent 58618 782f0b662cae
child 61416 b9a3324e4e62