src/HOL/FunDef.thy
changeset 52808 143f225e50f5
parent 49989 34d0ac1bdac6
child 53603 59ef06cda7b9
equal deleted inserted replaced
52807:b859a180936b 52808:143f225e50f5