src/HOL/Quot/HQUOT.thy
changeset 6180 99f107fd478f
parent 3842 b55686a7b22c