src/Doc/Implementation/Syntax.thy
changeset 82999 9dc2e3155257
parent 76987 4c275405faae