src/HOL/ex/Recdefs.thy
changeset 5253 82a5ca6290aa
parent 5124 1ce3cccfacdb
child 5502 da4d0444ea85