src/HOL/Tools/record.ML
changeset 61268 abe08fb15a12
parent 61260 e6f03fae14d5
child 61861 be63fa2b608e