src/HOL/Partial_Function.thy
changeset 45615 c05e8209a3aa
parent 45297 3c9f17d017bf
child 46041 1e3ff542e83e