src/HOL/Fun.ML
changeset 8862 78643f8449c6
parent 8767 eae30939b592
child 9108 9fff97d29837