src/Doc/Implementation/Syntax.thy
changeset 77907 ee9785abbcd6
parent 76987 4c275405faae