src/HOL/Recdef.thy
changeset 23063 b4ee6ec4f9c6
parent 22622 25693088396b
child 23150 073a65f0bc40