src/HOL/Recdef.thy
changeset 32176 893614e2c35c
parent 31723 f5cafe803b55
child 32244 a99723d77ae0