src/HOL/Fun_Def.thy
changeset 80813 9dd4dcb08d37
parent 80322 b10f7c981df6
equal deleted inserted replaced
80812:0f820da558f9 80813:9dd4dcb08d37