src/HOL/Partial_Function.thy
changeset 45524 43ca06e6c168
parent 45297 3c9f17d017bf
child 46041 1e3ff542e83e