src/HOL/Fun.ML
changeset 5533 bce36a019b03
parent 5441 45bd13b15d80
child 5608 a82a038a3e7a