src/HOL/FunDef.thy
changeset 49271 b08f9d534a2a
parent 48891 c0eafbd55de3
child 49989 34d0ac1bdac6