src/HOL/ex/Fundefs.thy
changeset 55430 8eb6c740ec1a
parent 53991 d8f7f3d998de
child 58249 180f1b3508ed
equal deleted inserted replaced
55429:4a50f9e70dc1 55430:8eb6c740ec1a