src/HOL/ex/Recdefs.thy
changeset 7087 67c6706578ed
parent 6481 dbf2d9b3d6c8
child 8415 852c63072334