src/HOL/ex/Recdefs.thy
changeset 5789 7d4ac02677a6
parent 5502 da4d0444ea85
child 6455 34c6c2944908