src/HOL/ex/Recdefs.thy
changeset 5526 e7617b57a3e6
parent 5502 da4d0444ea85
child 6455 34c6c2944908
equal deleted inserted replaced
5525:896f8234b864 5526:e7617b57a3e6