src/HOL/ex/Recdefs.thy
changeset 5944 dcc446da8e19
parent 5502 da4d0444ea85
child 6455 34c6c2944908