src/HOL/Fun.ML
changeset 5204 858da18069d7
parent 5148 74919e8f221c
child 5305 513925de8962