src/HOL/Tools/record.ML
changeset 52550 09e52d4a850a
parent 52230 1105b3b5aa77
child 52788 da1fdbfebd39