src/HOL/Tools/record.ML
changeset 59253 9448f4fc95e0
parent 59164 ff40c53d1af9
child 59266 776964a0589f