src/HOL/ex/Fundefs.thy
changeset 55487 6380313b8ed5
parent 53991 d8f7f3d998de
child 58249 180f1b3508ed