src/HOL/Fun_Def.thy
changeset 70665 94442fce40a5
parent 70520 11d8517d9384
child 71404 f2b783abfbe7
equal deleted inserted replaced
70664:2bd9e30183b1 70665:94442fce40a5