src/HOL/Tools/record.ML
changeset 46468 4db76d47b51a
parent 46223 cf91e1944229
child 46708 b138dee7bed3