src/HOL/Quot/HQUOT.thy
changeset 7983 d823fdcc0645
parent 3842 b55686a7b22c