src/HOL/Fun.thy
changeset 5526 e7617b57a3e6
parent 5305 513925de8962
child 5608 a82a038a3e7a