src/HOL/Fun.thy
changeset 63207 22bd3341b964
parent 63072 eb5d493a9e03
child 63322 bc1f17d45e91