src/HOL/Fun.ML
changeset 5242 3087dafb70ec
parent 5148 74919e8f221c
child 5305 513925de8962
equal deleted inserted replaced
5241:e5129172cb2b 5242:3087dafb70ec