src/HOL/Recdef.thy
changeset 22330 00ca68f5ce29
parent 22264 6a65e9b2ae05
child 22399 80395c2c40cc