src/HOL/Recdef.thy
changeset 22505 e2d378a97905
parent 22399 80395c2c40cc
child 22622 25693088396b