src/HOL/Recdef.thy
changeset 22588 4a859d13ef83
parent 22399 80395c2c40cc
child 22622 25693088396b