src/HOL/Recdef.thy
changeset 11565 ab004c0ecc63
parent 11533 0c0d2332e8f0
child 12023 d982f98e0f0d
equal deleted inserted replaced
11564:7b87c95fdf3b 11565:ab004c0ecc63