src/Doc/Implementation/Syntax.thy
changeset 64831 4792ee012e94
parent 61854 38b049cd3aad
child 69597 ff784d5a5bfb