src/HOL/Quot/HQUOT.ML
changeset 7025 afbd8241797b
parent 6162 484adda70b65