src/HOL/Tools/record_package.ML
changeset 7025 afbd8241797b
parent 6851 526c0b90bcef
child 7178 50b9849cf6ad
equal deleted inserted replaced
7024:44bd3c094fd6 7025:afbd8241797b