src/HOL/Fun.thy
changeset 71425 f2da99316b86
parent 71404 f2b783abfbe7
child 71464 4a04b6bd628b