src/HOL/Tools/Function/fun.ML
changeset 46936 571ce2bc0b64
parent 45639 efddd75c741e
child 46961 5c6955f487e5
equal deleted inserted replaced
46934:89cc3dfb383b 46936:571ce2bc0b64