src/HOL/Recdef.thy
changeset 23148 ef3fa1386102
parent 22622 25693088396b
child 23150 073a65f0bc40