src/HOL/Fun.ML
changeset 6986 82a4ac9c6b03
parent 6829 50459a995aa3
child 7014 11ee650edcd2