src/HOL/Fun_Def.thy
changeset 60724 4fce5d462afc
parent 60682 5a6cd2560549
child 60758 d8d85a8172b5