src/HOL/Tools/record.ML
changeset 36587 534418d8d494
parent 36173 99212848c933
child 36610 bafd82950e24