src/HOL/Tools/record.ML
changeset 46623 bce24d3f29e7
parent 46223 cf91e1944229
child 46708 b138dee7bed3