src/HOL/Fun_Def.thy
changeset 68217 3e90b88b0fc2
parent 67613 ce654b0e6d69
child 69605 a96320074298
equal deleted inserted replaced
68216:c0f86aee29db 68217:3e90b88b0fc2