src/HOL/Fun.thy
changeset 4271 3a82492e70c5
parent 4059 59c1422c9da5
child 4648 f04da668581c