src/HOL/ex/Fundefs.thy
changeset 56076 e52fc7c37ed3
parent 53991 d8f7f3d998de
child 58249 180f1b3508ed