src/HOL/Tools/record.ML
changeset 36316 f9b45eac4c60
parent 36173 99212848c933
child 36610 bafd82950e24