src/HOL/FunDef.thy
changeset 31456 55edadbd43d5
parent 30480 f3421e8379ab
child 31723 f5cafe803b55
equal deleted inserted replaced
31455:2754a0dadccc 31456:55edadbd43d5