src/HOL/Fun.ML
changeset 5253 82a5ca6290aa
parent 5148 74919e8f221c
child 5305 513925de8962