src/HOL/Fun_Def.thy
changeset 81575 cb57350beaa9
parent 80322 b10f7c981df6
equal deleted inserted replaced
81574:c4abe6582ee5 81575:cb57350beaa9