src/HOL/Fun_Def.thy
changeset 61534 a88e07c8d0d5
parent 61032 b57df8eecad6
child 61799 4cf66f21b764