src/HOL/Tools/record.ML
changeset 36928 637100169bc7
parent 36610 bafd82950e24
child 36945 9bec62c10714
equal deleted inserted replaced
36927:476a8d4f5c8b 36928:637100169bc7