src/HOL/FunDef.thy
changeset 33583 b5e0909cd5ea
parent 33471 5aef13872723
child 34228 bc0cea4cae52
equal deleted inserted replaced
33546:5e2d381b0695 33583:b5e0909cd5ea