src/HOL/Fun.thy
changeset 39214 49fc6c842d6c
parent 39213 297cd703f1f0
child 39302 d7728f65b353