src/HOL/Tools/record.ML
changeset 63045 c50c764aab10
parent 62969 9f394a16c557
child 63064 2f18172214c8