src/HOL/ex/Functions.thy
changeset 69470 c8c3285f1294
parent 66453 cc19f7ca2ed6
child 70468 8406a2c296e0