src/HOL/ex/Recdefs.ML
changeset 5253 82a5ca6290aa
parent 5124 1ce3cccfacdb
child 5518 654ead0ba4f7