src/HOL/Fun_Def.thy
changeset 58446 e89f57d1e46c
parent 58377 c6f93b8d2d8e
child 58819 aa43c6f05bca