src/HOL/Quot/HQUOT.thy
changeset 5083 beb21c000cb1
parent 3842 b55686a7b22c