src/HOL/Fun.ML
changeset 5592 64697e426048
parent 5441 45bd13b15d80
child 5608 a82a038a3e7a