src/HOL/Fun.thy
changeset 23853 2c69bb1374b8
parent 23738 3a801ffdc58c
child 23878 bd651ecd4b8a