src/HOL/ex/Fundefs.thy
changeset 24127 a56b6ed2e49c
parent 23817 ee3ee9ea0d34
child 24585 c359896d0f48