src/HOL/record.ML
changeset 4836 fc5773ae2790
parent 4574 b922012cc142
equal deleted inserted replaced
4835:f90a427d903f 4836:fc5773ae2790