src/HOL/Fun.thy
changeset 5565 301a3a4d3dc7
parent 5305 513925de8962
child 5608 a82a038a3e7a