src/Doc/Functions/Functions.thy
changeset 79100 e103e3cef3cb
parent 76987 4c275405faae