src/Doc/Implementation/Syntax.thy
changeset 73826 72900f34dbb3
parent 73764 35d8132633c6
child 76987 4c275405faae