src/HOL/Recdef.thy
changeset 31805 2f0adf64985b
parent 31723 f5cafe803b55
child 32244 a99723d77ae0
equal deleted inserted replaced
31802:a36b5e02c1ab 31805:2f0adf64985b