src/HOL/Tools/record.ML
changeset 36751 7f1da69cacb3
parent 36610 bafd82950e24
child 36945 9bec62c10714